From d1735b4914c43a50ff5c8d8c048a89f50ae33c4d Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Mon, 13 Apr 2020 15:43:13 +0200
Subject: Remove documentation for Hide menu in CoqIDE (was removed in 8.5).

---
 doc/sphinx/practical-tools/coqide.rst | 13 -------------
 1 file changed, 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
 -----------------------------------
 
-- 
cgit v1.2.3