diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-15 23:15:02 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-12-15 23:15:02 +0100 |
| commit | 33742251e62a49c7996b96ca7077cf985627d14b (patch) | |
| tree | e75d9166f963fdfa21ab754e2c9471909143ac60 /proofs/proof_global.ml | |
| parent | 7212e6c4a742110138a268650a59a67ef28d0582 (diff) | |
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.
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 3edd34e5f..c32e02344 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; |