diff options
| author | Clément Pit-Claudel | 2020-04-27 12:08:05 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-04-27 12:08:05 -0400 |
| commit | 040550c09033308f6c76b5630ee47fd9fab94327 (patch) | |
| tree | 72fe469b2503d1d0c6d72996564a94eaff66e49a /doc | |
| parent | f9f47108598fa2dfe705a4a58956803a4918bc52 (diff) | |
| parent | d1735b4914c43a50ff5c8d8c048a89f50ae33c4d (diff) | |
Merge PR #12090: Remove documentation for Hide menu in CoqIDE (was removed in 8.5).
Diffstat (limited to 'doc')
| -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 a69521c278..a045120b70 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -100,19 +100,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 ----------------------------------- |