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.

1 files changed, 5 insertions, 0 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