From e2789752960dabcda94e531f2c179446ad7dbb25 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 3 Mar 2018 01:58:48 +0100
Subject: [compat] Remove "Intuition Iff Unfolding"

Following up on #6791, we remove the option "Intuition Iff Unfolding"
---
 plugins/ltac/tauto.ml | 22 +++-------------------
 1 file changed, 3 insertions(+), 19 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 5ce30c3d7f..b9b84f3f48 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -63,11 +63,6 @@ let assoc_flags ist : tauto_flags =
 (* Whether inner not are unfolded *)
 let negation_unfolding = ref true
 
-(* Whether inner iff are unfolded *)
-let iff_unfolding = ref false
-
-let unfold_iff () = !iff_unfolding
-
 open Goptions
 let _ =
   declare_bool_option
@@ -77,14 +72,6 @@ let _ =
       optread  = (fun () -> !negation_unfolding);
       optwrite = (:=) negation_unfolding }
 
-let _ =
-  declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
-      optname  = "unfolding of iff in intuition";
-      optkey   = ["Intuition";"Iff";"Unfolding"];
-      optread  = (fun () -> !iff_unfolding);
-      optwrite = (:=) iff_unfolding }
-
 (** Base tactics *)
 
 let idtac = Proofview.tclUNIT ()
@@ -200,16 +187,13 @@ let make_unfold name =
   let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
   (Locus.AllOccurrences, ArgArg (EvalConstRef const, None))
 
-let u_iff = make_unfold "iff"
 let u_not = make_unfold "not"
 
 let reduction_not_iff _ ist =
   let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in
-  let tac = match !negation_unfolding, unfold_iff () with
-    | true, true -> make_reduce [u_not; u_iff]
-    | true, false -> make_reduce [u_not]
-    | false, true -> make_reduce [u_iff]
-    | false, false -> TacId []
+  let tac = match !negation_unfolding with
+    | true -> make_reduce [u_not]
+    | false -> TacId []
   in
   eval_tactic_ist ist tac
 
-- 
cgit v1.2.3