aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorThéo Zimmermann2019-01-24 16:35:24 +0100
committerThéo Zimmermann2019-01-24 16:35:24 +0100
commit1006fd52c03e7d8ea1d0b612df168f21c9b56455 (patch)
tree4652f89acf9f1fcf3818da68b88755a19c7c3861 /tactics
parent5a9aab76481e6ccaf311a02f18113af75eed3e7e (diff)
parentab7639ed91da9726f5248d9939db70df9ea18282 (diff)
Merge PR #9269: Move and rewrite intro pattern section
Ack-by: Zimmi48 Ack-by: anton-trunov Ack-by: jfehrle
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tactics.ml2
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);