Opened 11 years ago
Closed 11 years ago
#478 closed defect (fixed)
[Proof <body term>.] messes up following indentation
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | |
Cc: | jasongross9+pg@… |
Description
The following is some code indented with TAB:
Lemma foo : nat. Proof 1. Section Foo. End Foo. Lemma bar : Type. Proof forall x, x. Check bar.
Note: See
TracTickets for help on using
tickets.
Thanks, should be fixed in cvs.
Proof. Proof with foo.
are goal starters, but
Proo foo.
is not.