From 422bc59b8bb8276360843f8ee4dcb5e681ec220c Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Thu, 21 May 1998 17:27:00 +0000
Subject: Changing buffers now works.

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

diff --git a/todo b/todo
index 8da74d6e..87fe2e22 100644
--- a/todo
+++ b/todo
@@ -9,8 +9,8 @@ C (Low)    probably not worth wasting time on
 * This is a list of things which need doing in the generic interface
 ====================================================================
 
-A Structured review of complete system. Is there redundent code?
-  Can some of the LEGO/Coq specific code made generic? Reengineering.
+A Structured review of complete system. Is there redundant code?
+  Can some of the LEGO/Coq specific code made generic? Re-engineering.
     (2h hhg & tms)
 
 A Update source documentation and manual, in particular document bugs
@@ -57,6 +57,10 @@ C We need to go over to piped communication rather than ptys to fix
 C Outline-mode does not work due to read-only restrictions of
   protected region
 
+B Remove LEGO-specific code in proof.el: for example,
+  proof-shell-eager-annotation-end, proof-included-files-list.
+  (added by hhg)
+
 * Here are things to be done to Lego mode
 =========================================
 
@@ -112,5 +116,3 @@ A Add coq-add-tactic with a tactic name, which adds that tactic to the
 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