The Coq mailing list

[Gregory Malecha <gmalecha AT eecs.harvard.edu>]

You should be able to add -impredicative-set to your coq-prog-args variable. Something like:

(custom-set-variables

 '(coq-prog-args (quote ("-emacs-U" "-impredicative-set" ...)))

)

Hope this helps.

On Thu, Apr 14, 2011 at 10:56 AM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hello,

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

Vladimir.

--
gregory malecha