Proof using: do not clear unused section hyps automatically

The option is still there, but not documented since it is too
dangerous.  Hints and type classes instances are not taking cleared
variables into account.

1 files changed, 7 insertions, 7 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 481afa8f87..ed1b79e56e 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -186,7 +186,7 @@ in Section~\ref{ProofWith}.
 \subsubsection{{\tt Proof using} options}
 \optindex{Default Proof Using}
 \optindex{Suggest Proof Using}
-\optindex{Proof Using Clear Unused}
+% \optindex{Proof Using Clear Unused}
 
 The following options modify the behavior of {\tt Proof using}.
 
@@ -201,12 +201,12 @@ The following options modify the behavior of {\tt Proof using}.
   When {\tt Qed} is performed, suggest a {\tt using} annotation if
   the user did not provide one.
 
-\variant{\tt Unset Proof Using Clear Unused.}
-
-  When {\tt Proof using a} all section variables but for {\tt a} and
-  the variables used in the type of {\tt a} are cleared.
-  This option can be used to turn off this behavior.
-
+% \variant{\tt Unset Proof Using Clear Unused.}
+% 
+%   When {\tt Proof using a} all section variables but for {\tt a} and
+%   the variables used in the type of {\tt a} are cleared.
+%   This option can be used to turn off this behavior.
+% 
 \subsubsection[\tt Collection]{Name a set of section hypotheses for {\tt Proof using}}
 \comindex{Collection}\label{Collection}