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.

Change History (1)

comment:1 Changed 13 years ago by courtieu

Resolution: → fixed
Status: new → closed

This is fixed in cvs. Thanks for reporting.

Note: See TracTickets for help on using tickets.