From d020f9c42ad658b05d669e10aef03f43e1605a98 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Fri, 20 May 2011 06:38:04 +0000
Subject: - minor changes: clean personal todo list + adjust test case
 description

---
 coq/coq.el                               | 22 ----------------------
 coq/ex/test-cases/change-ancestor/README |  7 +++++--
 2 files changed, 5 insertions(+), 24 deletions(-)

diff --git a/coq/coq.el b/coq/coq.el
index ca07a53c..a6e34915 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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.
-- 
cgit v1.2.3