Added documentation for C-c C-s in Coq mode.

Fixed problem with tabbing changing buffers.

1 files changed, 0 insertions, 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