coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Pierre Courtieu <Pierre.Courtieu AT univ-orleans.fr>
To: Pierre Casteran <pierre.casteran AT labri.fr>
Cc: Stefan Monnier <monnier AT iro.umontreal.ca>, coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Re: impredicative with CoqIde
Date: Mon, 10 Jan 2005 11:46:20 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

listenOn 10 jan 2005, Pierre Casteran wrote:

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

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

Use the method  with Local Variables described in my previous mail. You can
specify any coqtop option (-I <path>, -impredicative-set ...).

What about the same kind of mechanism in Coq-ide?

Pierre

[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