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

1 files changed, 0 insertions, 12 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}