Opened 13 years ago

Closed 13 years ago

#373 closed defect (needmoreinfo)

PG 4.0 forgets things.

Reported by: megacz Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords:
Cc:

Description

Something is going very, very wrong with the proof state... see screenshot.

Attachments (1)

Screen shot 2010-10-06 at 11.11.12 PM.png (87.0 KB) - added by megacz 13 years ago.

Download all attachments as: .zip

Change History (2)

Changed 13 years ago by megacz

comment:1 Changed 13 years ago by David Aspinall

Resolution: needmoreinfo
Status: newclosed

Thanks for the report. It doesn't look good, but the screenshot provides nothing to go on.

Could you distill to a small example script please? (If that's hard, even the record of the session from the *coq* buffer would be more useful)

Note: See TracTickets for help on using tickets.