From 180b3739bb6601ff9aaf951e4b87e0bb45341b77 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:54:14 +0100
Subject: Deprecate options that were introduced for compatibility with 8.4.

---
 tactics/equality.ml | 2 +-
 tactics/tactics.ml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index d810e862af..6e56dc48e5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -67,7 +67,7 @@ let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "injection left-to-right pattern order and clear by default when with introduction pattern";
       optkey   = ["Injection";"L2R";"Pattern";"Order"];
       optread  = (fun () -> !injection_pattern_l2r_order) ;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index dbb613c40e..f56a913cbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -144,7 +144,7 @@ let use_bracketing_last_or_and_intro_pattern () =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "bracketing last or-and introduction pattern";
       optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
       optread  = (fun () -> !bracketing_last_or_and_intro_pattern);
-- 
cgit v1.2.3