Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Impredicative [ Set ]

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Impredicative [ Set ]


chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
  • To: Vladimir Voevodsky <vladimir AT ias.edu>
  • Cc: Gregory Malecha <gmalecha AT eecs.harvard.edu>, gmalecha AT cs.harvard.edu, Coq-Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Impredicative [ Set ]
  • Date: Fri, 15 Apr 2011 17:37:07 +0200
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=XaPQKSlU9M0sAeq0u2B+3CfbPlbXgYA23lkvS39m6/+dGwE8nyvNLqFXO1XZi6J17V ouT2ihoi7odgdDNkCGihzmiZXPki4cmQaujDHlmb9KYdwfpPKvCZcdCTjmeLtnDFAcgI Kavi6N6btS/438bPMY/oUGe9BpMk484fUueK4=

> (*
> *** Local Variables: ***
> *** coq-prog-name: "...." ***
> *** coq-prog-args: ("-emacs-U" "-impredicative-set")***
> *** End: ***
>  *)
> If one works with several files at the same time the PG applies the
> arguments, it seems, which are set in the first of the files loaded.
> Vladimir.

Hi,

More precisely, it applies the arguments present in the buffer in
which you *started* coq. If you want to start coq again for a file
with different arguments, you need to kill coq (C-c C-x or Coq > Exit
Coq) before scripting the new file.

<ad>
Notice that coq-prog-args use to be the place to also put "-I" options
but there is another way to set coq load path in trunk version of pg:

*** coq-load-path: ("/my/coq/dir/lib" "the/other/one") ***

This (experimental) mechanism, due to Hendrik Tews, allows pg to check
and recompile automatically modified dependencies when scripting a
"Require".
</ad>

Cheers,
Pierre Courtieu




Archive powered by MhonArc 2.6.16.

Top of Page