diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2011-01-21 09:59:35 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2011-01-21 09:59:35 +0000 |
| commit | e8e9187778549aa132b33321394345c99992b8b4 (patch) | |
| tree | 7df88deb31bf8572f90b345302011ce5bb90bf73 /coq/ex | |
| parent | 70140e80a12f3081cfc3fdf2c77ca759cc02dddc (diff) | |
- use time-less-p
- delete previous-head, simplify loop
- coq 8.2 compatibility
- describe bug for killing completely asserted active buffers in
coq/ex/test-cases/retract-completely-asserted
Diffstat (limited to 'coq/ex')
| -rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/README | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/coq/ex/test-cases/retract-completely-asserted/README b/coq/ex/test-cases/retract-completely-asserted/README index 68cca029..efdbdab0 100644 --- a/coq/ex/test-cases/retract-completely-asserted/README +++ b/coq/ex/test-cases/retract-completely-asserted/README @@ -18,3 +18,13 @@ To see that the example is indeed valid, script c.v. (For c.v you 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".) + +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 + apprears, and that the *coq* buffer is still live and that there is + no undo command in it +- visit b.v, do C-c C-n twice to get the error "a already exists" + +See "no deactivation-hooks when killing fully asserted active buffer" +on the pg-devel list. |