From 5c97a67f3227f718a2247c9476029548c4ee8e28 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Fri, 29 Jan 2010 14:18:31 +0000
Subject: 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
---
 theories/Numbers/Integer/Abstract/ZDivEucl.v  | 12 ++++++++----
 theories/Numbers/Integer/Abstract/ZDivFloor.v | 12 ++++++++----
 theories/Numbers/Integer/Abstract/ZDivTrunc.v |  2 +-
 3 files changed, 17 insertions(+), 9 deletions(-)

(limited to 'theories/Numbers/Integer/Abstract')

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
-- 
cgit v1.2.3