Added the btauto tactic to the documentation.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14921 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 24 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 5bcdae6e4..1334aa739 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,10 @@
+Changes from V8.4
+=================
+
+Tactics
+
+- Tactics btauto, a reflexive boolean tautology solver.
+
 Changes from V8.3 to V8.4
 =========================
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index c77260801..a8300da37 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3664,6 +3664,23 @@ congruence.
     described above.
 \end{ErrMsgs}
 
+\subsection{\tt btauto
+\tacindex{btauto}
+\label{btauto}}
+
+The tactic \texttt{btauto} implements a reflexive solver for boolean tautologies. It
+solves goals of the form {\tt t = u} where {\tt t} and {\tt u} are constructed
+over the following grammar:
+
+$$\mathtt{t} ::= x \mid \mathtt{true} \mid \mathtt{false}\mid \mathtt{orb\ t_1\ t_2}
+\mid \mathtt{andb\ t_1\ t_2} \mid\mathtt{xorb\ t_1\ t_2} \mid\mathtt{negb\ t}
+\mid\mathtt{if\ t_1\ then\ t_2\ else\ t_3}
+$$
+
+Whenever the formula supplied is not a tautology, it also provides a counter-example.
+
+Internally, it uses a system very similar to the one of the {\tt ring} tactic.
+
 \subsection{\tt omega
 \tacindex{omega}
 \label{omega}}