Numbers abstract layer: more Module Type, used especially for divisions.

 Properties are now rather passed as functor arg instead of via Include or
 some inner modules.

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

2 files changed, 9 insertions, 10 deletions

diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
index 473e25ffb..a7dcb63de 100644
--- a/theories/ZArith/ZOdiv.v
+++ b/theories/ZArith/ZOdiv.v
@@ -7,10 +7,9 @@
 (************************************************************************)
 
 
-Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing
- ZBinary ZDivTrunc Morphisms.
+Require Import BinPos BinNat Nnat ZArith_base ROmega ZArithRing Morphisms.
 Require Export ZOdiv_def.
-Require Zdiv.
+Require Zdiv ZBinary ZDivTrunc.
 
 Open Scope Z_scope.
 
@@ -247,7 +246,7 @@ Qed.
 (** We know enough to prove that [ZOdiv] and [ZOmod] are instances of
     one of the abstract Euclidean divisions of Numbers. *)
 
-Module ZODiv <: ZDiv ZBinAxiomsMod.
+Module ZODiv <: ZDivTrunc.ZDiv ZBinary.ZBinAxiomsMod.
  Definition div := ZOdiv.
  Definition modulo := ZOmod.
  Program Instance div_wd : Proper (eq==>eq==>eq) div.
@@ -259,12 +258,12 @@ Module ZODiv <: ZDiv ZBinAxiomsMod.
  Definition mod_opp_r := fun a b (_:b<>0) => ZOmod_opp_r a b.
 End ZODiv.
 
-Module ZODivMod := ZBinAxiomsMod <+ ZODiv.
+Module ZODivMod := ZBinary.ZBinAxiomsMod <+ ZODiv.
 
 (** We hence benefit from generic results about this abstract division. *)
 
 Module Z.
- Include ZDivPropFunct ZODivMod.
+ Include ZDivTrunc.ZDivPropFunct ZODivMod ZBinary.ZBinPropMod.
 End Z.
 
 (** * Unicity results *)
@@ -434,15 +433,15 @@ Proof. intros. zero_or_not b. apply Z.mod_le; auto with zarith. Qed.
 
 Theorem ZOdiv_le_upper_bound:
   forall a b q, 0 < b -> a <= q*b -> a/b <= q.
-Proof. intros a b q; rewrite mul_comm; apply Z.div_le_upper_bound. Qed.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_upper_bound. Qed.
 
 Theorem ZOdiv_lt_upper_bound:
   forall a b q, 0 <= a -> 0 < b -> a < q*b -> a/b < q.
-Proof. intros a b q; rewrite mul_comm; apply Z.div_lt_upper_bound. Qed.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.div_lt_upper_bound. Qed.
 
 Theorem ZOdiv_le_lower_bound:
   forall a b q, 0 < b -> q*b <= a -> q <= a/b.
-Proof. intros a b q; rewrite mul_comm; apply Z.div_le_lower_bound. Qed.
+Proof. intros a b q; rewrite Zmult_comm; apply Z.div_le_lower_bound. Qed.
 
 Theorem ZOdiv_sgn: forall a b,
   0 <= Zsgn (a/b) * Zsgn a * Zsgn b.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 06aa2b660..a07b6d038 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -319,7 +319,7 @@ Module ZDivMod := ZBinary.ZBinAxiomsMod <+ ZDiv.
 
 (** We hence benefit from generic results about this abstract division. *)
 
-Module Z := ZDivFloor.ZDivPropFunct ZDivMod.
+Module Z := ZDivFloor.ZDivPropFunct ZDivMod ZBinary.ZBinPropMod.
 
 
 (** Existence theorem *)