From e6fafcd7d4afc6e1d94a6db79d322499b2cb1b92 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 26 Jan 2011 10:43:52 +0000 Subject: - fix problem description --- coq/ex/test-cases/retract-completely-asserted/README | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'coq/ex') diff --git a/coq/ex/test-cases/retract-completely-asserted/README b/coq/ex/test-cases/retract-completely-asserted/README index efdbdab0..72e900c2 100644 --- a/coq/ex/test-cases/retract-completely-asserted/README +++ b/coq/ex/test-cases/retract-completely-asserted/README @@ -4,6 +4,11 @@ they are in different modules. To provoke an error inside ProofGeneral on correct coq input, do the following: +- Start a fresh emacs and delete (or comment out) the lines + (add-hook 'proof-deactivate-scripting-hook + 'coq-switch-buffer-kill-proof-shell + t) + in coq/coq.el. Safe that file. - Visit a.v and script the initial comment. - Set proof-no-fully-processed-buffer to nil. - assert buffer a.v completely @@ -19,6 +24,9 @@ either have to switch coq-recompile-before-require to t or you have to compile modules a and b yourself with "coqc a" and "coqc b".) +The following problem has been fixed by the commit of David Aspinall +around 2011-01-25 20:54:54 UTC. It can no longer be reproduced. + There is a bug present on 2011-01-21 09:49:36 UTC, to reproduce: - visit a.v, do C-c C-n twice to fully assert the buffer - kill buffer a.v, notice that there is no "coq killed" message -- cgit v1.2.3