The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Selon Stefan Monnier 
<monnier AT iro.umontreal.ca>:

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

Hmmm ... What about a bunch of modules, some of them with impredicative
Set, the others with the default predicativity :-) ?

>
>         Stefan
>
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>


-- 
Pierre Casteran
(+33) 540006931

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.