coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Venanzio Capretta writes:

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

coqide -impredicative-set

--
Jean-Christophe

[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