coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Build executables but not theories

From: "Edward Z. Yang" <ezyang AT mit.edu>
To: Tom Prince <tom.prince AT ualberta.net>
Cc: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Build executables but not theories
Date: Fri, 06 Apr 2012 03:26:29 -0400

Great, thank you very much!

Excerpts from Tom Prince's message of Fri Apr 06 00:33:23 -0400 2012:
> On Thu, 05 Apr 2012 23:26:50 -0400, "Edward Z. Yang"
> <ezyang AT mit.edu>
> wrote:
> > I'm doing some dev work on the Coq front-end, and it would be great
> > if I could tell Coq only to recompile those sources and not, for example,
> > all of the .v files.
>
> make coqbinaries
>
> > Alternatively, is there a way of running coqtop without any base
> > libraries?
>
> coqtop -nois

[Coq-Club] Build executables but not theories, Edward Z. Yang
- Re: [Coq-Club] Build executables but not theories, Tom Prince
  - Re: [Coq-Club] Build executables but not theories, Edward Z. Yang