The Coq mailing list

["Theodoros G. Tsokos" <T.Tsokos AT cs.bham.ac.uk>]

Dear all,

I would like to run ProofGeneral with option -impredicative-set. I tried 
the following two I found on a previous thread of Coq-Club:

1) To add this at the end of my file:

(*
*** Local Variables: ***
*** coq-prog-name: "coqtop -I . -emacs -impredicative-set" ***
*** End: ***
*)


2) To edit the "Menu -> ProofGeneral ->Advanced -> customize -> Coq -> 
Coq prog name".

On the first case, it still outputs: "User error: Needs option 
-impredicative-set" and on the second case it outputs: " Starting 
process: /usr/bin/coqtop.opt -impredicative-set -emacs-U..failed".

Any help/advice please? Thanks in advance,
Theo.