Merge PR #6898: [compat] Remove "Intuition Iff Unfolding"

2 files changed, 3 insertions, 31 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 6dca314b4..40ba43b6c 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4589,7 +4589,6 @@ incompatibilities.
 \end{Variants}
 
 \optindex{Intuition Negation Unfolding}
-\optindex{Intuition Iff Unfolding}
 
 Some aspects of the tactic {\tt intuition} can be
 controlled using options. To avoid that inner negations which do not
@@ -4609,17 +4608,6 @@ To do that all negations of the goal are unfolded even inner ones
 To avoid that inner occurrence of {\tt iff} which do not need to be
 unfolded are unfolded (this is the default), use:
 
-\begin{quote}
-{\tt Unset Intuition Iff Unfolding}
-\end{quote}
-
-To do that all negations of the goal are unfolded even inner ones
-(this is the default), use:
-
-\begin{quote}
-{\tt Set Intuition Iff Unfolding}
-\end{quote}
-
 % En attente d'un moyen de valoriser les fichiers de demos
 %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v}
 
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index d0f31cd42..a51c09ca4 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -65,11 +65,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
@@ -79,14 +74,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 ()
@@ -202,16 +189,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