From 2b4616438cc2a41e2c381ad47819d13addbd773c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 11 Jul 2017 17:16:15 +0200
Subject: 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.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f2baed905..1c60010cad 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);
-- 
cgit v1.2.3