diff options
| author | Healfdene Goguen | 1998-05-12 14:53:38 +0000 |
|---|---|---|
| committer | Healfdene Goguen | 1998-05-12 14:53:38 +0000 |
| commit | 2abec1102c6d5c37890ac938e978e6fc0b7ab14a (patch) | |
| tree | 5f1ef58658b9dda264c439e0b6a49e850116406b | |
| parent | aad4a48ea0de3de570cfd4af5905862afb090809 (diff) | |
Added documentation for C-c C-s in Coq mode.
| -rw-r--r-- | script-management.texinfo | 10 |
1 files 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 |