commit de field + renommages

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

9 files changed, 16 insertions, 16 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index 47be9d236..a21bfec44 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Export ZArith.
-Require Export NewZArithRing.
+Require Export ZArithRing.
 Require Export Setoid.
 
 (** * Definition of [Q] and basic properties *)
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 40c310ff4..ade0cd5eb 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import NewField Field_tac.
+Require Import Field Field_tac.
 Require Import QArith.
 Require Import Znumtheory.
 Require Import Eqdep_dec.
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v
index c05ea465d..a00d42879 100644
--- a/theories/Reals/ArithProp.v
+++ b/theories/Reals/ArithProp.v
@@ -12,7 +12,7 @@ Require Import Rbase.
 Require Import Rbasic_fun.
 Require Import Even.
 Require Import Div2.
-Require Import NewArithRing.
+Require Import ArithRing.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 3b5d241fa..c6feb4ac6 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -13,9 +13,9 @@
 (***************************************************************************)
 
 Require Export Raxioms.
-Require Export NewZArithRing.
+Require Export ZArithRing.
 Require Import Omega.
-Require Export Field_tac. Import NewField.
+Require Export Field_tac. Import Field.
 
 Open Local Scope Z_scope.
 Open Local Scope R_scope.
@@ -88,7 +88,7 @@ apply Rlt_trans with (0 + 1).
   apply Rplus_0_l.
 Qed.
 
-Lemma Rgen_phiPOS : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x > 0.
+Lemma Rgen_phiPOS : forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x > 0.
 unfold Rgt in |- *.
 induction x; simpl in |- *; intros.
  apply Rlt_trans with (1 + 0).
@@ -111,7 +111,8 @@ induction x; simpl in |- *; intros.
 Qed.
 
 
-Lemma Rgen_phiPOS_not_0 : forall x, ZRing_th.gen_phiPOS1 1 Rplus Rmult x <> 0.
+Lemma Rgen_phiPOS_not_0 :
+  forall x, InitialRing.gen_phiPOS1 1 Rplus Rmult x <> 0.
 red in |- *; intros.
 specialize (Rgen_phiPOS x).
 rewrite H in |- *; intro.
@@ -119,8 +120,8 @@ apply (Rlt_asym 0 0); trivial.
 Qed.
 
 Lemma Zeq_bool_complete : forall x y, 
-  ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
-  ZRing_th.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
+  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp x =
+  InitialRing.gen_phiZ 0%R 1%R Rplus Rmult Ropp y ->
   Zeq_bool x y = true.
 Proof gen_phiZ_complete _ _ _ _ _ _ _ _ _ _ Rset Rext Rfield Rgen_phiPOS_not_0.
 
diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v
index 878d5f73d..99c804272 100644
--- a/theories/Reals/Rfunctions.v
+++ b/theories/Reals/Rfunctions.v
@@ -15,8 +15,8 @@
 (**          Definition of the sum functions            *)
 (*                                                      *)
 (********************************************************)
-Require Export ArithRing. (* for ring_nat... *)
-Require Export NewArithRing.
+Require Export LegacyArithRing. (* for ring_nat... *)
+Require Export ArithRing.
 
 Require Import Rbase.
 Require Export R_Ifp.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 718ac3b03..a3f17f4d8 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -8,8 +8,7 @@
 
 (*i $Id$ i*)
 
-Require Import NewZArithRing.
-
+Require Import ZArithRing.
 Require Import ZArith_base.
 Require Import Omega.
 Require Import Wf_nat.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 52f85eada..d08515e62 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 NewZArithRing.
+Require Import ZArithRing.
 Require Import Zcomplements.
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 14bfa6357..9ae354eae 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 Require Import ZArith_base.
-Require Import NewZArithRing.
+Require Import ZArithRing.
 Require Import Zcomplements.
 Require Import Zdiv.
 Require Import Ndigits.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt.v
index 3d57561ea..804ab679d 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Import NewZArithRing.
+Require Import ZArithRing.
 Require Import Omega.
 Require Export ZArith_base.
 Open Local Scope Z_scope.