Opened 12 years ago
Closed 11 years ago
#451 closed defect (fixed)
support {} and bullets in prooftree
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | |
Cc: | hendrik@… |
Description
see subject
Change History (3)
comment:1 Changed 12 years ago by
Milestone: | PG-Emacs-4.2 → PG-Emacs-4.3 |
---|
comment:2 Changed 12 years ago by
comment:3 Changed 11 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
The necessary changes have been implemented now.
Hendrik
Note: See
TracTickets for help on using
tickets.
This requires more work than I thought. The problem is that with braces and bullets Coq exhibits a state where the old current goal has been finished but it has not yet switched to the next goal. Without braces and bullets you never see such a state and prooftree cannot handle it.