From c3adbee017f79d6fac40c217e0a6efdfb377d5ce Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Wed, 6 Oct 1999 10:51:07 +0000
Subject: Updates

---
 doc/ProofGeneral.texi | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

(limited to 'doc')

diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index d3bce47f..a28bef39 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -2023,7 +2023,6 @@ General.
 
 @node Coq-specific commands
 @section Coq-specific commands
-@kindex C-c C-s
 @kindex C-c I 
 @kindex C-c a
 @kindex C-c s
@@ -2035,9 +2034,6 @@ Coq Proof General supplies the following key-bindings:
 Inserts ``Intros '' into proof buffer.
 @item C-c a
 Inserts ``Apply '' into proof buffer.
-@item C-c C-s
-Runs Coq's search utility on a user-provided string, using
-the @code{Search} command of Coq.
 @item C-c s
 Inserts ``Section '' into proof buffer
 @item C-c e
@@ -2086,7 +2082,7 @@ recognize.
 
 @node Suggested Coq abbreviations
 @section Suggested Coq abbreviations
-@c could be generic
+@c FIXME: could make this generic
 
 Coq has many command strings that are long, such as ``Reflexivity,''
 ``Inductive,'' ``Definition'' and ``Discriminate.''  Although it is
-- 
cgit v1.2.3