From bd1c976531ad6154339fff7e48e85dbe7951de23 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 9 Sep 2015 11:20:04 +0200
Subject: Activating bracketing of last or-and introduction pattern by default
 for more regularity.

---
 CHANGES            | 5 +++++
 tactics/tactics.ml | 2 +-
 2 files changed, 6 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3