diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 31 |
2 files changed, 27 insertions, 9 deletions
@@ -23,6 +23,11 @@ Tactics - New compatibility flag "Universal Lemma Under Conjunction" which let tactics working under conjunctions apply sublemmas of the form "forall A, ... -> A". +- New compatibility flag "Bracketing Last Introduction Pattern" which can be + set so that the last disjunctive-conjunctive introduction pattern given to + "intros" automatically complete the introduction of its subcomponents, as the + the disjunctive-conjunctive introduction patterns in non-terminal position + already do. API diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 3d6928d032..e27e7c4023 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -126,6 +126,26 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } +(* The following boolean governs what "intros []" do on examples such + as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; + if false, it behaves as "intro H; case H; clear H" for fresh H. + Kept as false for compatibility. + *) + +let bracketing_last_or_and_intro_pattern = ref false + +let use_bracketing_last_or_and_intro_pattern () = + !bracketing_last_or_and_intro_pattern + && Flags.version_strictly_greater Flags.V8_4 + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "bracketing last or-and introduction pattern"; + optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; + optread = (fun () -> !bracketing_last_or_and_intro_pattern) ; + optwrite = (fun b -> bracketing_last_or_and_intro_pattern := b) } (*********************************************) (* Tactics *) @@ -2191,17 +2211,10 @@ and prepare_intros_loc loc dft = function let intro_patterns_bound_to n destopt = intro_patterns_core true [] [] [] destopt - (Some (true,n)) 0 (fun _ -> clear_wildcards) - -(* The following boolean governs what "intros []" do on examples such - as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; - if false, it behaves as "intro H; case H; clear H" for fresh H. - Kept as false for compatibility. - *) -let bracketing_last_or_and_intro_pattern = false + (Some (true,n)) 0 (fun _ l -> clear_wildcards l) let intro_patterns_to destopt = - intro_patterns_core bracketing_last_or_and_intro_pattern + intro_patterns_core (use_bracketing_last_or_and_intro_pattern ()) [] [] [] destopt None 0 (fun _ l -> clear_wildcards l) let intro_pattern_to destopt pat = |