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"
---
 doc/refman/RefMan-tac.tex | 12 ------------
 1 file changed, 12 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9635b3ab1a..56f8d34e90 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}
 
-- 
cgit v1.2.3