Opened 13 years ago

Closed 13 years ago

#395 closed defect (fixed)

proof-segment-up-to-using-cache broken since Oct 11 20:07:17 2010 +0200

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

Description

Hi,

the changeset 7913:9ebd4b14cadc committed on Oct 11 20:07:17 2010 +0200 breaks the cache. To reproduce, open the attached coq file and

  1. do proof-process-buffer, which yields an error because there are two declarations peirce
  2. change the first peirce into peirce_1 and do proof-process-buffer again. The error persists, because Proof General sent peirce instead of peirce_1 to the prover. Further the locked region ends in the middle of an identifier.

Bye,

Hendrik Tews

Attachments (1)

peirce.v​ (225 bytes) - added by coquser 13 years ago.

Download all attachments as: .zip

Change History (4)

Changed 13 years ago by coquser

Attachment: peirce.v​ added

comment:1 Changed 13 years ago by David Aspinall

Thanks for the test case. This patch was indeed a bit ropey. I've tweaked it a bit but it still could do with some testing so leaving this open for now. We should add some test cases in the autotest to try to cover this.

comment:2 Changed 13 years ago by David Aspinall

Minor issue: #401

comment:3 Changed 13 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Closing now, no problems seen after a fair bit of testing.

Note: See TracTickets for help on using tickets.