From 33742251e62a49c7996b96ca7077cf985627d14b Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 15 Dec 2015 23:15:02 +0100
Subject: 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.
---
 proofs/proof_global.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

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;
-- 
cgit v1.2.3