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.

5 files changed, 12 insertions, 9 deletions

diff --git a/CHANGES b/CHANGES
index b39d84ba57..a3cec81c1a 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,6 +20,7 @@ Tactics
 - Syntax "p/c" for on-the-fly application of a lemma c before
   introducing along pattern p changed to p%c1..%cn. The feature and
   syntax are in experimental stage.
+- "Proof using" does not clear unused section variables.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
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}
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 3edd34e5f6..c32e02344d 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -254,7 +254,7 @@ let start_dependent_proof id ?pl str goals terminator =
 let get_used_variables () = (cur_pstate ()).section_vars
 let get_universe_binders () = (cur_pstate ()).universe_binders
 
-let proof_using_auto_clear = ref true
+let proof_using_auto_clear = ref false
 let _ = Goptions.declare_bool_option
     { Goptions.optsync  = true;
       Goptions.optdepr  = false;
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index c83f45e2a4..adaa05ad06 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -178,6 +178,7 @@ End Let.
 
 Check (test_let 3).
 
+(* Disabled
 Section Clear.
 
 Variable a: nat.
@@ -192,6 +193,6 @@ trivial.
 Qed.
 
 End Clear.
-
+*)
 
 
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index fe18686e21..443dd683d2 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -970,6 +970,7 @@ Section Map.
   Lemma in_flat_map : forall (f:A->list B)(l:list A)(y:B),
     In y (flat_map f l) <-> exists x, In x l /\ In y (f x).
   Proof using A B.
+    clear Hfinjective.
     induction l; simpl; split; intros.
     contradiction.
     destruct H as (x,(H,_)); contradiction.