diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 12 |
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} |