diff options
| -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. |