diff options
author | 2017-07-11 17:16:15 +0200 | |
---|---|---|
committer | 2017-07-11 17:16:15 +0200 | |
commit | 2b4616438cc2a41e2c381ad47819d13addbd773c (patch) | |
tree | 811b5494a56ccf1ec38b1ec2140451f9931a4151 /tactics | |
parent | fbbcea2eda411fbacfafdeec3266a19af17935f3 (diff) |
Backtracking on deprecation of Bracketing Last Intro Pattern.
As per @JasonGross's request who described a use case for this option in
https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative
solution for this use case.
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 6f2baed90..1c60010ca 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -143,7 +143,7 @@ let use_bracketing_last_or_and_intro_pattern () = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) + { optdepr = false; optname = "bracketing last or-and introduction pattern"; optkey = ["Bracketing";"Last";"Introduction";"Pattern"]; optread = (fun () -> !bracketing_last_or_and_intro_pattern); |