From f5de32ad1600cd18a6f1f286729c979e868ad088 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 11:32:54 +0100
Subject: Documenting options "Intuition Negation Unfolding", "Intuition Iff
 Unfolding".

---
 doc/refman/RefMan-tac.tex | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ce934871f3..b07cfb7d59 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4233,6 +4233,38 @@ incompatibilities.
   Is equivalent to {\tt intuition auto with *}.
 \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
+need to be unfolded are unfolded, use:
+
+\begin{quote}
+{\tt Unset Intuition Negation 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 Negation Unfolding}
+\end{quote}
+
+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