From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:08:14 +0100
Subject: Remove support for Coq 8.2.

---
 vernac/indschemes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78e..e90c259263 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -92,7 +92,7 @@ let _ = (* compatibility *)
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
 
-let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+let is_eq_flag () = !eq_flag
 
 let eq_dec_flag = ref false 
 let _ =
-- 
cgit v1.2.3


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.

---
 vernac/indschemes.ml    |  7 -------
 vernac/vernacentries.ml | 11 -----------
 2 files changed, 18 deletions(-)

(limited to 'vernac')

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index e90c259263..44d6f37cc6 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,13 +84,6 @@ let _ =
       optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
-let _ = (* compatibility *)
-  declare_bool_option
-    { optdepr  = true;
-      optname  = "automatic declaration of boolean equality";
-      optkey   = ["Equality";"Scheme"];
-      optread  = (fun () -> !eq_flag) ;
-      optwrite = (fun b -> eq_flag := b) }
 
 let is_eq_flag () = !eq_flag
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b75..9978848ff3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1394,17 +1394,6 @@ let _ =
       optread  = (fun () -> !CClosure.share);
       optwrite = (fun b -> CClosure.share := b) }
 
-(* No more undo limit in the new proof engine.
-   The command still exists for compatibility (e.g. with ProofGeneral) *)
-
-let _ =
-  declare_int_option
-    { optdepr  = true;
-      optname  = "the undo limit (OBSOLETE)";
-      optkey   = ["Undo"];
-      optread  = (fun _ -> None);
-      optwrite = (fun _ -> ()) }
-
 let _ =
   declare_bool_option
     { optdepr  = false;
-- 
cgit v1.2.3


From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Tue, 22 Nov 2016 17:51:32 +0100
Subject: Deprecate options that were introduced for compatibility with 8.2.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9978848ff3..ba1da655a8 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1298,7 +1298,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic introduction of variables";
       optkey   = ["Automatic";"Introduction"];
       optread  = Flags.is_auto_intros;
-- 
cgit v1.2.3