Opened 12 years ago
Closed 12 years ago
#431 closed defect (needmoreinfo)
"This subproof is complete" appears at bottom of goals
| Reported by: | Robin Green | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | trivial | Milestone: | PG-Emacs-4.2 |
| Component: | 7:prover-coq | Keywords: | |
| Cc: |
Description
After a bulleted subproof has been completed,
This subproof is complete, but there are still unfocused goals:
appears at the bottom of the goals window. It should either appear at the top, or not at all.
Change History (1)
comment:1 Changed 12 years ago by
| Resolution: | → needmoreinfo |
|---|---|
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Could you upload a simple example please? (So non Coq user may try)