From 57d85bc149dab955b5e1834ecbfe814d34d34db4 Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Tue, 12 May 1998 14:55:07 +0000
Subject: Added documentation for C-c C-s in Coq mode. Fixed problem with
 tabbing changing buffers.

---
 todo | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/todo b/todo
index 0bcf82e1..ec5d09d3 100644
--- a/todo
+++ b/todo
@@ -60,8 +60,6 @@ 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
 
-A <tab> can change buffers now!  At least in Coq mode.
-
 * Here are things to be done to Lego mode
 =========================================
 
@@ -99,8 +97,6 @@ B Add Patrick Loiseleur's commands to search for vernac or ml files.
 
 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