mise a jour du nouveau ring et ajout du nouveau field, avant renommages

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

4 files changed, 10 insertions, 9 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index d3b8a37f03..718ac3b031 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,7 +8,8 @@
 
 (*i $Id$ i*)
 
-Require Import ZArithRing.
+Require Import NewZArithRing.
+
 Require Import ZArith_base.
 Require Import Omega.
 Require Import Wf_nat.
@@ -209,4 +210,4 @@ End Zlength_properties.
 
 Implicit Arguments Zlength_correct [A].
 Implicit Arguments Zlength_cons [A].
-Implicit Arguments Zlength_nil_inv [A].
\ No newline at end of file
+Implicit Arguments Zlength_nil_inv [A].
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 025e03d4af..52f85eada8 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -22,7 +22,7 @@ Then only after proves the main required property.
 Require Export ZArith_base.
 Require Import Zbool.
 Require Import Omega.
-Require Import ZArithRing.
+Require Import NewZArithRing.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
@@ -148,7 +148,7 @@ case (Zgt_bool b (2 * r)); rewrite BinInt.Zpos_xO;
  (split; [ ring | omega ]).
 
 generalize (Zge_cases b 2).
-case (Zge_bool b 2); (intros; split; [ ring | omega ]).
+case (Zge_bool b 2); (intros; split; [ try ring | omega ]).
 omega.
 Qed.
 
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 05076ebd34..14bfa6357a 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Import ZArith_base.
-Require Import ZArithRing.
+Require Import NewZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
 Require Import Ndigits.
@@ -164,7 +164,7 @@ left; rewrite H0; rewrite e; ring.
 assert (Hqq0 : q0 * q = 1).
 apply Zmult_reg_l with a.
 assumption.
-ring.
+ring_simplify.
 pattern a at 2 in |- *; rewrite H2; ring.
 assert (q | 1).
 rewrite <- Hqq0; auto with zarith.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index f61999362f..3d57561ea5 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -8,9 +8,9 @@
 
 (* $Id$ *)
 
+Require Import NewZArithRing.
 Require Import Omega.
 Require Export ZArith_base.
-Require Export ZArithRing.
 Open Local Scope Z_scope.
 
 (**********************************************************************)
@@ -86,7 +86,7 @@ refine
             end
         end
     end); clear sqrtrempos; repeat compute_POS;
- try (try rewrite Heq; ring; fail); try omega.
+ try (try rewrite Heq; ring); try omega.
 Defined.
 
 (** Define with integer input, but with a strong (readable) specification. *)
@@ -132,7 +132,7 @@ refine
                (fun r:Z => 0 = 0 * 0 + r /\ 0 * 0 <= 0 < (0 + 1) * (0 + 1)) 0
                _)
     end); try omega.
-split; [ omega | rewrite Heq; ring ((s + 1) * (s + 1)); omega ].
+split; [ omega | rewrite Heq; ring_simplify ((s + 1) * (s + 1)); omega ].
 Defined.
 
 (** Define a function of type Z->Z that computes the integer square root,