Opened 13 years ago
Closed 13 years ago
#386 closed defect (fixed)
Coq goals counter not reset on backtracking out of proof
Reported by: | David Aspinall | Owned by: | courtieu |
---|---|---|---|
Priority: | major | Milestone: | PG-Emacs-4.1 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
Test case with example.v
: process to split, then retract open proof by C-c C-RET to Goal. Modeline indicator still shows 2 open goals.
Note: See
TracTickets for help on using
tickets.
This is fixed in cvs. Thanks for reporting.