Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def

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

3 files changed, 7 insertions, 10 deletions

diff --git a/plugins/setoid_ring/Cring.v b/plugins/setoid_ring/Cring.v
index 367958a6b3..1f7915eebf 100644
--- a/plugins/setoid_ring/Cring.v
+++ b/plugins/setoid_ring/Cring.v
@@ -11,7 +11,6 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import BinList.
 Require Import Znumtheory.
-Require Import Zdiv_def.
 Require Export Morphisms Setoid Bool.
 Require Import ZArith.
 Require Export Algebra_syntax.
@@ -81,7 +80,7 @@ Lemma cring_power_theory :
 intros; apply Ring_theory.mkpow_th. reflexivity. Defined.
 
 Lemma cring_div_theory: 
-  div_theory _==_ Zplus Zmult gen_phiZ Zquotrem.
+  div_theory _==_ Zplus Zmult gen_phiZ Z.quotrem.
 intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
 simpl.   apply ring_setoid. Defined.
 End cring.
@@ -109,7 +108,7 @@ Ltac cring_gen :=
                         (fun n:N => n)
                         (@Ring_theory.pow_N _  1 multiplication)
                         cring_power_theory
-                        Zquotrem
+                        Z.quotrem
                         cring_div_theory
                         O fv nil);
                  let rc := fresh "rc"in
diff --git a/plugins/setoid_ring/Cring_tac.v b/plugins/setoid_ring/Cring_tac.v
index c7f0ae7791..f7e1a284d0 100644
--- a/plugins/setoid_ring/Cring_tac.v
+++ b/plugins/setoid_ring/Cring_tac.v
@@ -11,7 +11,6 @@ Require Import Setoid.
 Require Import BinPos.
 Require Import BinList.
 Require Import Znumtheory.
-Require Import Zdiv_def.
 Require Export Morphisms Setoid Bool.
 Require Import ZArith.
 Open Scope Z_scope.
@@ -164,7 +163,7 @@ Lemma cring_power_theory :  forall (R:Type)(Rr:Cring R),
 intros; apply mkpow_th; set_cring_notations. rrefl. Defined.
 
 Lemma cring_div_theory: forall (R:Type)(Rr:Cring R),
-  div_theory cring_eq Zplus Zmult (gen_phiZ Rr) Zquotrem.
+  div_theory cring_eq Zplus Zmult (gen_phiZ Rr) Z.quotrem.
 intros. apply InitialRing.Ztriv_div_th. unfold Setoid_Theory.
 simpl.   apply (@cring_setoid R Rr). Defined.
 
@@ -189,7 +188,7 @@ Ltac cring_gen :=
                         Z 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool
                         (@gen_phiZ _ _) (@cring_morph _ _) N (fun n:N => n)
                         (@Ring_theory.pow_N _  1 multiplication)
-                        (@cring_power_theory _ _) Zquotrem (@cring_div_theory _ _) O fv nil);
+                        (@cring_power_theory _ _) Z.quotrem (@cring_div_theory _ _) O fv nil);
                       set_cring_notations;
                       let rc := fresh "rc"in
                         intro rc; apply rc
diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 9e4ac94b4c..763dbe7b92 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -13,7 +13,6 @@ Require Import BinNat.
 Require Import Setoid.
 Require Import Ring_theory.
 Require Import Ring_polynom.
-Require Import Zdiv_def.
 Import List.
 
 Set Implicit Arguments.
@@ -591,11 +590,11 @@ Qed.
 
  Variable zphi : Z -> R.
 
- Lemma Ztriv_div_th : div_theory req Zplus Zmult zphi Zquotrem.
+ Lemma Ztriv_div_th : div_theory req Z.add Z.mul zphi Z.quotrem.
  Proof.
   constructor.
-  intros; generalize (Zquotrem_eq a b); case Zquotrem; intros; subst.
-  rewrite Zmult_comm; rsimpl.
+  intros; generalize (Z.quotrem_eq a b); case Z.quotrem; intros; subst.
+  rewrite Z.mul_comm; rsimpl.
  Qed.
 
  Variable nphi : N -> R.