coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] impredicative with CoqIde

From: Lionel Elie Mamane <lionel AT mamane.lu>
To: Venanzio Capretta <Venanzio.Capretta AT mathstat.uottawa.ca>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] impredicative with CoqIde
Date: Mon, 10 Jan 2005 04:10:16 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

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".

--
Lionel

[Coq-Club] impredicative with CoqIde, Venanzio Capretta
- Re: [Coq-Club] impredicative with CoqIde, Jean-Christophe Filliatre
- [Coq-Club] Re: impredicative with CoqIde, Stefan Monnier
  - Re: [Coq-Club] Re: impredicative with CoqIde, Pierre Casteran
    - Re: [Coq-Club] Re: impredicative with CoqIde, Pierre Courtieu
      - [Coq-Club] Re: impredicative with CoqIde, Stefan Monnier
        
        Re: [Coq-Club] Re: impredicative with CoqIde, Pierre Courtieu
    - [Coq-Club] Re: impredicative with CoqIde, Stefan Monnier
- Re: [Coq-Club] impredicative with CoqIde, Lionel Elie Mamane
  - Re: [Coq-Club] impredicative with CoqIde, Pierre Courtieu