Custom Query (361 matches)

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.

If you have the below code, then place the caret at the end of the "Case" line and press Ctrl+J (or Enter, TAB), Emacs will spin up and use 100% of the CPU. This is on 4.1-RC4.

Theorem rev_snoc : forall X : Type, 
                     forall v : X,
                     forall s : list X,
  rev (snoc s v) = v :: (rev s).
Proof.
  simpl.
  intros X v s.
  induction s as [|s'].
  Case "s=nil".

  reflexivity.
  Qed.

displaying this customization group gives an error and a lot of options are invisible