From 8de84e8e7bc394bf231ca9164d7e3951d6edfae0 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond <guillaume.melquiond@inria.fr>
Date: Thu, 21 Sep 2017 15:22:26 +0200
Subject: Mark "Set Tactic Compat Context" as deprecated.

It was introduced in 8.5 for compatibility with a 8.4 bug.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5698312ae..d0165c555 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -74,7 +74,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "trigger bugged context matching compatibility";
       optkey   = ["Tactic";"Compat";"Context"];
       optread  = (fun () -> !Flags.tactic_context_compat) ;
-- 
cgit v1.2.3