Opened 13 years ago

Closed 13 years ago

#416 closed defect (fixed)

Emacs indentation can go into an infinite loop

Reported by: coquser Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 2:pg-emacs Keywords:
Cc:

Description

Paste the following code in. After the final period, press either Ctrl+J or enter followed by tab. Emacs (Aquamacs or GNU Emacs 23) will spin up one processor to 100% and run forever. 

Theorem binaryUnaryCommute' : forall b : bin,
  convert (succ (b)) = convert b + 1.
Proof.
  intros b.
  induction b as [| b' | b'].
  Case "b = BO".

Change History (1)

comment:1 Changed 13 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Thanks for the report. Now patched.

Note: See TracTickets for help on using tickets.