Activating bracketing of last or-and introduction pattern by default

for more regularity.

2 files changed, 6 insertions, 1 deletions

diff --git a/CHANGES b/CHANGES
index 5d6dd69c60..10ec10a5e4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,8 @@
+Changes beyond V8.5
+===================
+
+- Flag "Bracketing Last Introduction Pattern" is now on by default.
+
 Changes from V8.5beta2 to V8.5beta3
 ===================================
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 221c661b21..c26ea56784 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -146,7 +146,7 @@ let _ =
    Kept as false for compatibility.
  *)
 
-let bracketing_last_or_and_intro_pattern = ref false
+let bracketing_last_or_and_intro_pattern = ref true
 
 let use_bracketing_last_or_and_intro_pattern () =
   !bracketing_last_or_and_intro_pattern