diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
2 files changed, 6 insertions, 1 deletions
@@ -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 |