Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.S

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

5 files changed, 30 insertions, 16 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index d0f530fef9..bcd16fec6c 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -37,15 +37,19 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Z' <: NZDivSig.
-  Include Z.
+ Module ZD <: NZDiv Z.
+  Definition div := div.
+  Definition modulo := modulo.
+  Definition div_wd := div_wd.
+  Definition mod_wd := mod_wd.
+  Definition div_mod := div_mod.
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof.
   intros. rewrite <- (abs_eq b) at 3 by now apply lt_le_incl.
   apply mod_always_pos.
   Qed.
- End Z'.
- Module Import NZDivP := NZDivPropFunct Z' ZP.
+ End ZD.
+ Module Import NZDivP := NZDivPropFunct Z ZP ZD.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index b94affd798..1e7624ba64 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -41,12 +41,16 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Z' <: NZDivSig.
-  Include Z.
+ Module ZD <: NZDiv Z.
+  Definition div := div.
+  Definition modulo := modulo.
+  Definition div_wd := div_wd.
+  Definition mod_wd := mod_wd.
+  Definition div_mod := div_mod.
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. intros. now apply mod_pos_bound. Qed.
- End Z'.
- Module Import NZDivP := NZDivPropFunct Z' ZP.
+ End ZD.
+ Module Import NZDivP := NZDivPropFunct Z ZP ZD.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 6b6b717035..3200ba2af3 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -42,7 +42,7 @@ Module ZDivPropFunct (Import Z : ZDivSig')(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := NZDivPropFunct Z ZP.
+ Module Import NZDivP := NZDivPropFunct Z ZP Z.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index b189d5b298..1f6c615bc3 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -43,11 +43,13 @@ End NZDivSpecific.
 Module Type NZDiv (NZ:NZOrdAxiomsSig)
  := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ.
 
-Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv.
-Module Type NZDivSig' := NZOrdAxiomsSig' <+ NZDiv <+ DivModNotation.
+Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ.
 
 Module NZDivPropFunct
- (Import NZ : NZDivSig')(Import NZP : NZMulOrderPropSig NZ).
+ (Import NZ : NZOrdAxiomsSig')
+ (Import NZP : NZMulOrderPropSig NZ)
+ (Import NZD : NZDiv' NZ)
+.
 
 (** Uniqueness theorems *)
 
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index dd033fb764..0cb5665acb 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -21,12 +21,16 @@ Module NDivPropFunct (Import N : NDivSig')(Import NP : NPropSig N).
 
 (** We benefit from what already exists for NZ *)
 
- Module N' <: NZDivSig.
-  Include N.
+ Module ND <: NZDiv N.
+  Definition div := div.
+  Definition modulo := modulo.
+  Definition div_wd := div_wd.
+  Definition mod_wd := mod_wd.
+  Definition div_mod := div_mod.
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. split. apply le_0_l. apply mod_upper_bound. order. Qed.
- End N'.
- Module Import NZDivP := NZDivPropFunct N' NP.
+ End ND.
+ Module Import NZDivP := NZDivPropFunct N NP ND.
 
  Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l.