coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Florian Hatat <florian.hatat AT ens-lyon.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] impredicative-set in proof general
- Date: Mon, 19 May 2008 12:04:41 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Theodoros G. Tsokos wrote:
> > 1) To add this at the end of my file:
> >
> > (*
> > *** Local Variables: ***
> > *** coq-prog-name: "coqtop -I . -emacs -impredicative-set" ***
> > *** End: ***
> > *)
>
With ProofGeneral 3.7, I use:
(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U" "-impredicative-set") ***
*** End: ***
*)
--
Florian,
http://openweb.eu.org/
http://www.linux-france.org/
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] impredicative-set in proof general, Theodoros G. Tsokos
- Re: [Coq-Club] impredicative-set in proof general, Florian Hatat
Archive powered by MhonArc 2.6.16.