Custom Query (361 matches)

The issue is that after changing the active scripting buffer, the first assert operation is lost, because the prover is not running. To reproduce go to coq/ex/test-cases/multiple-files-single-dir and do some scripting in, say, a.v. Then change to a different file (eg b.v) and do some scripting there. To clearly see the effect, make sure the second file (b.v) does not start with a comment.

There is a patch in ​http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000114.html but it needs reviewing.

Hi,

this docstring mentions the callbacks init-cmd and interactive-input. These seem not to exist any more. It does not mention proof-shell-set-silent and proof-shell-clear-silent.

Bye,

Hendrik Tews

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