From ac2b757a7835672ba494bf42244b5d393e8db089 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Thu, 7 Dec 2017 22:27:19 +0100
Subject: Remove deprecated option Tactic Compat Context.

And some code simplification.
---
 tactics/tactics.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cc5593f3f2..bf05c9b834 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,14 +59,6 @@ let typ_of env sigma c =
 
 open Goptions
 
-let _ =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "trigger bugged context matching compatibility";
-      optkey   = ["Tactic";"Compat";"Context"];
-      optread  = (fun () -> !Flags.tactic_context_compat) ;
-      optwrite = (fun b -> Flags.tactic_context_compat := b) }
-
 let apply_solve_class_goals = ref false
 
 let _ =
-- 
cgit v1.2.3