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 coquser

Resolution: invalid
Status: newclosed

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.

comment:2 Changed 10 years ago by coquser

Resolution: invalid
Status: closedreopened

It happens in Coq with BackTo? as well.

Last edited 10 years ago by coquser (previous) (diff)

comment:3 Changed 10 years ago by coquser

Resolution: invalid
Status: reopenedclosed
Note: See TracTickets for help on using tickets.