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.

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 5eacb1a95e..c6cc955b0f 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -66,7 +66,7 @@ let negation_unfolding = ref true
 (* Whether inner iff are unfolded *)
 let iff_unfolding = ref false
 
-let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2
+let unfold_iff () = !iff_unfolding
 
 open Goptions
 let _ =
-- 
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.

---
 plugins/ltac/tauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index c6cc955b0f..2a8ed72387 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -79,7 +79,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "unfolding of iff in intuition";
       optkey   = ["Intuition";"Iff";"Unfolding"];
       optread  = (fun () -> !iff_unfolding);
-- 
cgit v1.2.3