Opened 10 years ago
Closed 10 years ago
#495 closed defect (invalid)
Goals buffer aggressively cleared with Coq pre-8.5
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | |
Cc: | johnw@… |
Description
I am using Proof General 4.3pre131011 with the current trunk version of Coq (pre-8.5).
With 8.4pl4, if I type period to end a tactic, my goals buffer update. If I delete the period, the goals buffer changes to what it had displayed immediately before. This is the desired behavior.
With 8.5pre, when I delete the period it clears the goals buffer, and does not display again until I press the period, making it extremely difficult to replay what changes a certain tactic made to my environment.
Change History (3)
comment:1 Changed 10 years ago by
Resolution: | → invalid |
---|---|
Status: | new → closed |
comment:2 Changed 10 years ago by
Resolution: | invalid |
---|---|
Status: | closed → reopened |
It happens in Coq with BackTo? as well.
comment:3 Changed 10 years ago by
Resolution: | → invalid |
---|---|
Status: | reopened → closed |
Note: See
TracTickets for help on using
tickets.
I've tracked down what is going on, and it looks like a Coq issue: Calls to Backtrack are not reprinting the goal. I will pursue this bug on the Coq bug tracker.