The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Hi,

I don't know if I understand you but when I use Impredicative Set mode I
run coq (at Microsoft Windows) in this way:

cd "C:\Program Files\Coq\bin\"

coqtop -impredicative-set

Greetings,

Marko Malikoviæ

> Hello,
>
> is there a way to turn on the "Impredicative Set" option in the
> interactive mode (e.g. in Proof General)?
>
> Vladimir.
>
>
>


-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------