From 2abec1102c6d5c37890ac938e978e6fc0b7ab14a Mon Sep 17 00:00:00 2001
From: Healfdene Goguen
Date: Tue, 12 May 1998 14:53:38 +0000
Subject: Added documentation for C-c C-s in Coq mode.

---
 script-management.texinfo | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/script-management.texinfo b/script-management.texinfo
index 2b26ea9f..dda36fdf 100644
--- a/script-management.texinfo
+++ b/script-management.texinfo
@@ -354,7 +354,8 @@ print LEGO help text in the response buffer
 
 @end table
 
-In addition, there are some abbreviations for common commands
+In addition, there are some abbreviations for common commands, which
+add text to the buffer:
 
 @table @kbd
 @item C-c i   
@@ -377,12 +378,17 @@ As well as custom popup menus, it has the following commands:
 @item C-c C-p
 display the proof state in the response buffer
 
+@item C-c C-s
+search for items in the library of a given type.  This runs the
+@kbd{Search} command of Coq.
+
 @item C-c c
 display the context in the response buffer
 
 @end table
 
-In addition, there are some abbreviations for common commands:
+In addition, there are some abbreviations for common commands, which
+add text to the buffer:
 
 @table @kbd
 @item C-c I   
-- 
cgit v1.2.3