diff options
| author | Hugo Herbelin | 2015-09-09 11:20:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-11-10 16:38:51 +0100 |
| commit | bd1c976531ad6154339fff7e48e85dbe7951de23 (patch) | |
| tree | 432374009e0a63b7e64a9d75114ccda2173e933d /tactics | |
| parent | 2bad1e8d896b40495bc8579e407f142f7f3fb7d9 (diff) | |
Activating bracketing of last or-and introduction pattern by default
for more regularity.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |