More precise description of boolean ring in doc (see bug #2401)

Also remove misleading example about classical propositional logic in
"What does this tactic do?" section.

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

1 files changed, 2 insertions, 6 deletions

diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 94c76c197..3898bf4c4 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -37,11 +37,6 @@ commutativity.
 \begin{Examples}
 \item In the ring of integers, the normal form of 
 $x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$.
-\item For the classical propositional calculus (or the boolean rings)
-  the normal form is what logicians call \textit{disjunctive normal
-    form}: every formula is equivalent to a disjunction of
-  conjunctions of atoms. (Here $\oplus$ is $\vee$, $\otimes$ is
-  $\wedge$, variables are atoms and the only constants are T and F)
 \end{Examples}
 
 \texttt{ring} is also able to compute a normal form modulo monomial 
@@ -660,7 +655,8 @@ Coq Reference Manual, version 8.0.
 This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
 associative commutative rewriting on every ring.  The tactic must be
 loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
-the \texttt{Add Ring} command. The ring of booleans
+the \texttt{Add Ring} command. The ring of booleans (with \texttt{andb}
+as multiplication and \texttt{xorb} as addition)
 is predefined; if one wants to use the tactic on \texttt{nat} one must
 first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do
 \texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require