Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] impredicative with CoqIde

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] impredicative with CoqIde


chronological Thread 
  • From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
  • To: Lionel Elie Mamane <lionel AT mamane.lu>
  • Cc: Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>, coq-club AT pauillac.inria.fr
  • Subject: Re: [Coq-Club] impredicative with CoqIde
  • Date: Mon, 10 Jan 2005 09:55:01 +0100
  • List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
On 10 jan 2005, Lionel Elie Mamane wrote:

> On Fri, Jan 07, 2005 at 08:10:35AM -0500, Venanzio Capretta wrote:
> 
> >  how can I specify the option -impredicative-set when using
> > ProofGeneral?
> 
> Menu "Proof-General", advanced, customize, coq, coq prog name. There,
> add all options you want, set, save. Then menu "coq", "exit coq".
> 

If you do not want to do this each time you open your file, put this at its
end (complete with other options):

(*
*** Local Variables: ***
*** coq-prog-name: "coqtop -I . -emacs -impredicative-set" ***
*** End: ***
*)

Pierre Courtieu


Archive powered by MhonArc 2.6.16.

Top of Page