Added proof folding into CoqIde. See RefMan for using it.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11814 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 1 deletions

diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index fa66d8336d..fd112f6fa2 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -103,9 +103,20 @@ the preferences.
 These tactics are general ones, in particular they do not refer to
 particular hypotheses. You may also try specific tactics related to
 the goal or one of the hypotheses, by clicking with the right mouse
-button one the goal or the considered hypothesis. This is the
+button on the goal or the considered hypothesis. This is the
 ``contextual menu on goals'' feature, that may be disabled in the
 preferences if undesirable.
+
+\section{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 \texttt{Hide} entry of the \texttt{Navigation}
+menu, or with a mouse right-click. The proof shall be enclosed between \texttt{Proof.}
+and \texttt{Qed.}, both with their final dots. Finally, the proof that shall be hidden
+or revealed is the first one whose \texttt{Lemma},\texttt{Theorem} or \texttt{Definition}
+statement precedes the insert cursor.
  
 \section{Vernacular commands, templates}