diff options
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 1043c50f00..070b2356e5 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -98,7 +98,7 @@ let use_bracketing_last_or_and_intro_pattern () = let () = declare_bool_option - { optdepr = false; + { optdepr = true; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); |