Custom Query (361 matches)

This has been a bug in PG for several years now, but as far as I can see I haven't reported it before.

If you select or deselect the setting Print Fully Explicit, and then immediately do proof-undo-last-successful-command, the setting will be reverted to its previous state, but PG still thinks it is enabled (or disabled, whichever you set it to be).

I don't know if this also occurs with other settings.

If I recall correctly, you can get back in sync again by toggling the option in emacs, which has no effect on Coq.

Hello! I use Proof General with Coq, Utoks mode is enabled.

When I enter a string:

Case "".<newline>

Emacs stops responding. It's really annoying, since it's used in the course I'm trying to go through: ​http://www.cis.upenn.edu/~bcpierce/sf/Basics.html#lab28

I can reproduce a bug on my PC:

1. visit a new (or old) file with .v extension
2. type:

Case "".

3. Press "enter" button on keyboard (that is, to make new line)

Please help me with that!

I'm neither an Emacs nor Proof-General pro, so I'm not sure what should I do and what should I tell you.

I have some relevant to PG settings in my .emacs.d/init.el file:

(require 'unicode-tokens)

(add-hook 'coq-mode-hook
          (lambda ()
            (proof-unicode-tokens-enable)
            ))

(add-hook 'unicode-tokens-mode-hook
          (lambda ()
            (unicode-tokens-show-symbols)
            (local-set-key (kbd "s-v") 'unicode-tokens-paste)))

I use PG 4.1RC2. Emacs: GNU Emacs 24.0.50.1 (i386-apple-darwin10.7.3, NS apple-appkit-1038.35) on Mac OS X Lion.

http://proofgeneral.inf.ed.ac.uk/download#prereq says that emacs 23.1 or later is required, but 4.1RC2 requires version 23.3 or later:

In toplevel form:
coq/coq.el:443:24:Error: reference to free variable `smie-rules-function'
make[1]: *** [coq/coq.elc] Error 1