From 3f95f37c64e21134aa909f7adaf3a8141fe12fd8 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Tue, 5 May 1998 14:29:39 +0000
Subject: Coq now restarts if going back to beginning of proof.

---
 todo | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/todo b/todo
index f916e77e..049b11fe 100644
--- a/todo
+++ b/todo
@@ -88,15 +88,13 @@ A Error messages need to be revised e.g., if an import fails, LEGO
 * Here are things to be done to Coq mode
 ========================================
 
-A Restart if going back to beginning of proof. (30min hhg)
-
 ? There's a bug so the goal buffer isn't displaying everything that
   happens.
 
 C Sections and files are handled incorrectly.
 
 A Update documentation to include C-c C-s. (10min hhg)
- 
+
 A Lifted nested lemmas respond incorrectly to C-c u: Coq gets sent the
   correct command if I undo up to the lower lemma, but the buffer
   undoes to the upper lemma.  I.e., if I start Lemma x, then prove
-- 
cgit v1.2.3