aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-03 01:58:48 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2018-03-03 07:15:44 +0100
commite2789752960dabcda94e531f2c179446ad7dbb25 (patch)
treefa6f68a6ceebf17c177fc3b33b1bad0f60d4405f /doc
parentdf9d3a36e71d6d224286811fdc529ad5a955deb7 (diff)
[compat] Remove "Intuition Iff Unfolding"
Following up on #6791, we remove the option "Intuition Iff Unfolding"
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-tac.tex12
1 files changed, 0 insertions, 12 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9635b3ab1..56f8d34e9 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}