Opened 12 years ago
Closed 12 years ago
#450 closed defect (fixed)
Proof in proof tree
| Reported by: | coquser | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-4.2 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: | hendrik@… |
Description
With 8.4 Proof appears as command in the proof tree.
Hendrik
Note: See
TracTickets for help on using
tickets.
Fixed by ignoring Lemma, Definition and others and requiring that proofs are started with Proof. Because the latter is recommend practice, see Coq problem report 2776.