diff options
| author | David Aspinall | 1999-10-06 10:51:07 +0000 |
|---|---|---|
| committer | David Aspinall | 1999-10-06 10:51:07 +0000 |
| commit | c3adbee017f79d6fac40c217e0a6efdfb377d5ce (patch) | |
| tree | d9a5040f0b1394cb309e618bb3fca400090a82f0 /doc | |
| parent | 17c4857e9613cc3b820d30199e6107ebf90f859a (diff) | |
Updates
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/ProofGeneral.texi | 6 |
1 files changed, 1 insertions, 5 deletions
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 |