diff options
author | 2018-03-03 01:58:48 +0100 | |
---|---|---|
committer | 2018-03-03 07:15:44 +0100 | |
commit | e2789752960dabcda94e531f2c179446ad7dbb25 (patch) | |
tree | fa6f68a6ceebf17c177fc3b33b1bad0f60d4405f /doc | |
parent | df9d3a36e71d6d224286811fdc529ad5a955deb7 (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.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} |