coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Guard Condition, Christian Doczkal
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- Re: [Coq-Club] Guard Condition,
Gert Smolka
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- [Coq-Club] Impredicative [ Set ],
Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ],
Gregory Malecha
- Message not available
- Message not available
- Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ], Gregory Malecha
- Re: [Coq-Club] Impredicative [ Set ], Vladimir Voevodsky
- Re: [Coq-Club] Impredicative [ Set ], Pierre Courtieu
- Message not available
- [Coq-Club] messy behavior with universes, Vladimir Voevodsky
- [Coq-Club] Re: [coqdev] messy behavior with universes, Tom Prince
- [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Carlos Simpson
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Vladimir Voevodsky
- Message not available
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Enrico Tassi
- Re: [Coq-Club] Impredicative [ Set ],
Gregory Malecha
- Message not available
- Re: [Coq-Club] Re: [coqdev] messy behavior with universes, Andreas Abel
- [Coq-Club] THedu'11 at CADE: last call for ext.abstracts, Laurent Théry
- [Coq-Club] Impredicative [ Set ],
Vladimir Voevodsky
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- Re: [Coq-Club] Guard Condition,
Gert Smolka
- RE: [Coq-Club] Guard Condition,
Georges Gonthier
- [Coq-Club] an issue with notations, Vladimir Voevodsky
- [Coq-Club] a problem with canonical structures, Vladimir Voevodsky
Archive powered by MhonArc 2.6.16.