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.