diff options
| -rw-r--r-- | coq/coq.el | 22 | ||||
| -rw-r--r-- | coq/ex/test-cases/change-ancestor/README | 7 |
2 files changed, 5 insertions, 24 deletions
@@ -954,28 +954,6 @@ This is specific to `coq-mode'." ;; Multiple file handling revisited ;; -;; TODO list: -;; - Bug: assert newly appended text in locked ancestor apparently -;; sends text before killing coqtop -;; (unreported) -;; - Bug: undo in locked ancestor -;; - Bug: never stopping busy cursor -;; - modify behavior of locked ancestors, see proof-span-read-only -;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000094.html) -;; - fix problem with partial library names -;; - set completion-ignored-extensions -;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000122.html) -;; - avoid restarting coqtop when the load path does not change -;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000088.html) -;; - defpacustom customization groups -;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000115.html) -;; - broken pg cache (http://proofgeneral.inf.ed.ac.uk/trac/ticket/395) -;; - do not kill coqtop when unlocking ancestors -;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000138.html) -;; - don't move point in invisible scripting buffer -;; (http://lists.inf.ed.ac.uk/pipermail/proofgeneral-devel/2011/000139.html) - - ;; user options and variables (defgroup coq-auto-compile () diff --git a/coq/ex/test-cases/change-ancestor/README b/coq/ex/test-cases/change-ancestor/README index 056bd892..91dc814d 100644 --- a/coq/ex/test-cases/change-ancestor/README +++ b/coq/ex/test-cases/change-ancestor/README @@ -16,8 +16,11 @@ To reproduce the test do the following: This test case triggers a bug in the cvs version from -2011-05-12 12:10:00 UTC. The bug is that after unlocking the -ancestor a.v only the newly added text is sent to Coq. Therefore +2011-05-12 12:10:00 UTC. The bug has been fixed, see issue +http://proofgeneral.inf.ed.ac.uk/trac/ticket/400 . + +The bug is that after unlocking the +ancestor a.v, only the newly added text is sent to Coq. Therefore Coq responds with an error (reference a was not found in the current environment). When one asserts a.v from the beginning, the definition of b is of course accepted. |