diff options
| author | Théo Zimmermann | 2020-04-13 15:43:13 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-13 15:43:13 +0200 |
| commit | d1735b4914c43a50ff5c8d8c048a89f50ae33c4d (patch) | |
| tree | c9ebbaf6d2dece2af6ffc9732194369837b708dd | |
| parent | 0beca74bc90cef03d779a8e4f8668335c9c37716 (diff) | |
Remove documentation for Hide menu in CoqIDE (was removed in 8.5).
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index b1f392c337..ab3d70eaca 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -98,19 +98,6 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -Proof folding ------------------- - -As your script grows bigger and bigger, it might be useful to hide the -proofs of your theorems and lemmas. - -This feature is toggled via the Hide entry of the Navigation menu. The -proof shall be enclosed between ``Proof.`` and ``Qed.``, both with their final -dots. The proof that shall be hidden or revealed is the first one -whose beginning statement (such as ``Theorem``) precedes the insertion -cursor. - - Vernacular commands, templates ----------------------------------- |