From dc32141739045df2eebdd649802f815470b58a15 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Wed, 26 Nov 1997 17:15:23 +0000
Subject: A few new suggestions

---
 todo | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/todo b/todo
index 333ba114..35982946 100644
--- a/todo
+++ b/todo
@@ -24,3 +24,18 @@ This is a list of things which need doing to the lego mode.
 
 * LEGO mode might incorporate changes to Coq mode menu, in particular
   making help refer to the info file.
+
+* LEGO and Coq modes overwrite each other.
+
+Here are things to be done to Coq mode:
+
+* Restart if going back to beginning of proof.
+
+* C-c u inside a Section should reset the whole section, then redo defns
+
+* There's a bug so the goal buffer isn't displaying everything that
+  happens.
+
+* Sections and files are handled incorrectly.
+
+* Update documentation to include C-c C-s.
-- 
cgit v1.2.3