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 | |
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.
-rw-r--r-- | CHANGES | 1 | ||||
-rw-r--r-- | doc/refman/RefMan-pro.tex | 14 | ||||
-rw-r--r-- | proofs/proof_global.ml | 2 | ||||
-rw-r--r-- | test-suite/success/proof_using.v | 3 | ||||
-rw-r--r-- | theories/Lists/List.v | 1 |
5 files changed, 12 insertions, 9 deletions
@@ -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 481afa8f8..ed1b79e56 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 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; diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v index c83f45e2a..adaa05ad0 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 fe18686e2..443dd683d 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. |