The Coq mailing list

[Stefan Monnier <monnier AT iro.umontreal.ca>]

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

But that doesn't work if the coqtop process is already executing from
another Proof-General session.


        Stefan