complement du commit 9591

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

3 files changed, 17 insertions, 9 deletions

diff --git a/.depend.coq b/.depend.coq
index 62b939e5d..2b627f7c2 100644
--- a/.depend.coq
+++ b/.depend.coq
@@ -374,12 +374,13 @@ contrib/setoid_ring/Ring_theory.vo: contrib/setoid_ring/Ring_theory.v theories/S
 contrib/setoid_ring/Ring_polynom.vo: contrib/setoid_ring/Ring_polynom.v theories/Setoids/Setoid.vo contrib/setoid_ring/BinList.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/BinInt.vo contrib/setoid_ring/Ring_theory.vo
 contrib/setoid_ring/Ring_tac.vo: contrib/setoid_ring/Ring_tac.v theories/Setoids/Setoid.vo theories/NArith/BinPos.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/newring.cmo
 contrib/setoid_ring/Ring_base.vo: contrib/setoid_ring/Ring_base.v contrib/setoid_ring/newring.cmo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/InitialRing.vo
-contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_polynom.vo
+contrib/setoid_ring/InitialRing.vo: contrib/setoid_ring/InitialRing.v theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo theories/ZArith/BinInt.vo theories/NArith/BinNat.vo theories/Setoids/Setoid.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/Ring_zdiv.vo
 contrib/setoid_ring/Ring_equiv.vo: contrib/setoid_ring/Ring_equiv.v contrib/ring/Setoid_ring_theory.vo contrib/ring/LegacyRing_theory.vo contrib/setoid_ring/Ring_theory.vo
 contrib/setoid_ring/Ring.vo: contrib/setoid_ring/Ring.v theories/Bool/Bool.vo contrib/setoid_ring/Ring_theory.vo contrib/setoid_ring/Ring_base.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Ring_tac.vo
 contrib/setoid_ring/ArithRing.vo: contrib/setoid_ring/ArithRing.v theories/Arith/Mult.vo theories/NArith/BinNat.vo theories/NArith/Nnat.vo contrib/setoid_ring/Ring.vo
 contrib/setoid_ring/NArithRing.vo: contrib/setoid_ring/NArithRing.v contrib/setoid_ring/Ring.vo theories/NArith/BinPos.vo theories/NArith/BinNat.vo
 contrib/setoid_ring/ZArithRing.vo: contrib/setoid_ring/ZArithRing.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo theories/ZArith/Zpow_def.vo
+contrib/setoid_ring/Ring_zdiv.vo: contrib/setoid_ring/Ring_zdiv.v theories/NArith/BinPos.vo theories/NArith/BinNat.vo theories/ZArith/ZArith_base.vo
 contrib/setoid_ring/Field_theory.vo: contrib/setoid_ring/Field_theory.v contrib/setoid_ring/Ring.vo theories/ZArith/ZArith_base.vo
 contrib/setoid_ring/Field_tac.vo: contrib/setoid_ring/Field_tac.v contrib/setoid_ring/Ring_tac.vo contrib/setoid_ring/BinList.vo contrib/setoid_ring/Ring_polynom.vo contrib/setoid_ring/InitialRing.vo contrib/setoid_ring/Field_theory.vo
 contrib/setoid_ring/Field.vo: contrib/setoid_ring/Field.v contrib/setoid_ring/Field_theory.vo contrib/setoid_ring/Field_tac.vo
diff --git a/Makefile b/Makefile
index 05a3327f9..c9156cb17 100644
--- a/Makefile
+++ b/Makefile
@@ -1084,7 +1084,7 @@ NEWRINGVO=\
  contrib/setoid_ring/Ring_base.vo 	contrib/setoid_ring/InitialRing.vo \
  contrib/setoid_ring/Ring_equiv.vo 	contrib/setoid_ring/Ring.vo \
  contrib/setoid_ring/ArithRing.vo	contrib/setoid_ring/NArithRing.vo \
- contrib/setoid_ring/ZArithRing.vo \
+ contrib/setoid_ring/ZArithRing.vo 	contrib/setoid_ring/Ring_zdiv.vo \
  contrib/setoid_ring/Field_theory.vo	contrib/setoid_ring/Field_tac.vo \
  contrib/setoid_ring/Field.vo		contrib/setoid_ring/RealField.vo
 
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 2a885290c..e81a0e964 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -1,6 +1,6 @@
 \achapter{The \texttt{ring} and \texttt{field} tactic families}
-\aauthor{Bruno Barras, Benjamin Gr\'egoire and Assia
-  Mahboubi\footnote{based on previous work from
+\aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia
+  Mahboubi, Laurent Th\'ery\footnote{based on previous work from
   Patrick Loiseleur and Samuel Boutin}}
 \label{ring}
 \tacindex{ring}
@@ -8,7 +8,6 @@
 This chapter presents the tactics dedicated to deal with ring and
 field equations.
 
-
 \asection{What does this tactic?}
 
 \texttt{ring} does associative-commutative rewriting in ring and semi-ring
@@ -46,8 +45,8 @@ $x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$.
 \end{Examples}
 
 \texttt{ring} is also able to compute a normal form modulo monomial 
-equalities. For example, under the hypothesis that $x^2 = yz$,
- the normal form of $(x + 1)x - x - zy$ is 0.
+equalities. For example, under the hypothesis that $2x^2 = yz+1$,
+ the normal form of $2(x + 1)x - x - zy$ is $x+1$.
 
 \asection{The variables map}
 
@@ -112,6 +111,7 @@ above to the terms given. The tactic then replaces all occurrences of
 the terms given in the conclusion of the goal by their normal
 forms. If no term is given, then the conclusion should be an equation
 and both hand sides are normalized. 
+The tactic can also be applied in a hypothesis.
 
 The tactic must be loaded by \texttt{Require Import Ring}. The ring
 structures must be declared with the \texttt{Add Ring} command (see
@@ -141,8 +141,8 @@ intros; ring.
 Abort.
 \end{coq_eval}
 \begin{coq_example}
-Goal forall a b:Z, a*b = 0 ->
-        (a+b)^2 = a^2 + b^2.
+Goal forall a b:Z, 2*a*b = 30 ->
+        (a+b)^2 = a^2 + b^2 + 30.
 \end{coq_example}
 \begin{coq_example}
 intros a b H; ring [H].
@@ -337,6 +337,8 @@ describes their syntax and effects:
   {\tt contrib/setoid\_ring/RealField.v} for examples.
   By default the tactic does not recognize power expressions as ring
   expressions.
+\item[sign {\term}]
+\item[div {\term}]
   
   
 \end{description}
@@ -513,6 +515,11 @@ apply. There is only one specific modifier:
   on coefficients w.r.t. the field equality.
 \end{description}
 
+{\tt field_simplify_eq}
+
+{\tt field_simplify}
+
+
 \asection{Legacy implementation}
 
 \Warning This tactic is the {\tt ring} tactic of previous versions of