The Coq mailing list

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

If you edited it outside of the emacs menus, then you'll probably need to close emacs and restart it (make sure that it doesn't revert your changes). There might be a way to do this without restarting emacs, but I don't know what it is.

On Thu, Apr 14, 2011 at 3:41 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

Hi,

I tried it and something (???) seems to reverse any changes to this variable.  I get the original line with the info:

String: -emacs-U

   State: CHANGED outside Customize; operating on it here may be unreliable.

   Arguments to be passed to `proof-prog-name' to run the proof assistant. More

while the saved one is -emacs-U -impredicative-set

Any ideas? (I tried doing it both through "Customization" and by introducing an extra line in .emacs). 

Thanks,

Vladimir. 

On Apr 14, 2011, at 11:22 AM, Gregory Malecha wrote:

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

-- 
gregory malecha