diff options
| author | Théo Zimmermann | 2019-01-24 16:35:24 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-01-24 16:35:24 +0100 |
| commit | 1006fd52c03e7d8ea1d0b612df168f21c9b56455 (patch) | |
| tree | 4652f89acf9f1fcf3818da68b88755a19c7c3861 /tactics | |
| parent | 5a9aab76481e6ccaf311a02f18113af75eed3e7e (diff) | |
| parent | ab7639ed91da9726f5248d9939db70df9ea18282 (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.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); |
