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)
Change History (2)
Changed 13 years ago by
Attachment: | Screen shot 2010-10-06 at 11.11.12 PM.png added |
---|
comment:1 Changed 13 years ago by
Resolution: | → needmoreinfo |
---|---|
Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
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)