coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: impredicative with CoqIde

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Re: impredicative with CoqIde
Date: Fri, 07 Jan 2005 13:09:59 -0500
Cancel-lock: sha1:KywlWeJSHmMos5WoXlPJwVUbJao=
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

>   how can I specify the option -impredicative-set when using CoqIde
>   or ProofGeneral?

It would be cleaner if the `impredicative-set' option could be set in the
source files rather than on the command line.

        Stefan

[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