From 553e23b317adc6b2f340b191b24bf5d60ba6de90 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Thu, 21 May 1998 08:30:07 +0000
Subject: Fixed lifting globals. Added problem of buffers and need for
 incremental adding of tactics in Coq.

---
 todo | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/todo b/todo
index b093ef4c..8da74d6e 100644
--- a/todo
+++ b/todo
@@ -103,14 +103,14 @@ A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
 
 B Proof-by-Pointing (10h hhg)
 
+A Add coq-add-tactic with a tactic name, which adds that tactic to the 
+  undoable tactics and to the font-lock. (2h hhg)
+
 * Emacs19
 =========
 
-A proof-lift-global doesn't work correctly.  This seems to relate to
-  the behavior of delete-region and insert with respect to overlays:
-  inserting at the beginning of an overlay in emacs19 may extend 
-  that overlay, whereas in xemacs it doesn't. (2hr hhg)
-
 B The proof-locked-span isn't set to read-only, because overlays don't 
   have that capability.  This needs to be done with text-regions.
   (2hr hhg)
+
+A Switching buffers doesn't work correctly. (1h hhg)
-- 
cgit v1.2.3