New option "Unset Bracketing Last Introduction Pattern" for preserving

compatibility with the non uniform behavior that "intros [] []" on
"A*B->C*D->E" automatically introduces A and B but leaves C and D in
the goal.

Kept unset in 8.5 but planned to be set in 8.6.

2 files changed, 27 insertions, 9 deletions

diff --git a/CHANGES b/CHANGES
index 08484a4b9b..70ddb81f4d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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 =