diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-26 10:43:52 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-26 10:43:52 +0000 |
| commit | e6fafcd7d4afc6e1d94a6db79d322499b2cb1b92 (patch) | |
| tree | a97ab2678485186ded53f750dd4cfccc85733bb6 /coq/ex | |
| parent | 7a1436160e556908160a513908c9a919343efb97 (diff) | |
- fix problem description
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/README | 8 |
1 files changed, 8 insertions, 0 deletions
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 |