Fixed lifting globals.

Added problem of buffers and need for incremental adding of tactics in
Coq.

1 files 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)