From 376da97be60957b25e59afb5791fae665127b17b Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:48:14 +0100
Subject: Remove options deprecated since 8.4.

---
 pretyping/unification.ml | 13 +------------
 1 file changed, 1 insertion(+), 12 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index ef4f7f7545..b4964c1f36 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -248,20 +248,9 @@ let sort_eqns = unify_r2l
 
 let global_pattern_unification_flag = ref true
 
-(* Compatibility option introduced and activated in Coq 8.3 whose
-   syntax is now deprecated. *)
-
 open Goptions
-let _ =
-  declare_bool_option
-    { optdepr  = true;
-      optname  = "pattern-unification for existential variables in tactics";
-      optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
-      optread  = (fun () -> !global_pattern_unification_flag);
-      optwrite = (:=) global_pattern_unification_flag }
 
-(* Compatibility option superseding the previous one, introduced and
-   activated in Coq 8.4 *)
+(* Compatibility option introduced and activated in Coq 8.4 *)
 
 let _ =
   declare_bool_option
-- 
cgit v1.2.3