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

6 files changed, 14 insertions, 15 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 3429a4fa3..64a122c71 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -15,7 +15,7 @@ Require Export ZAxioms.
 Require Import NZProperties.
 
 Module ZBasePropFunct (Import Z : ZAxiomsSig).
-Include NZPropFunct Z.
+Include Type NZPropFunct Z.
 Local Open Scope NumScope.
 
 (* Theorems that are true for integers but not for natural numbers *)
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index ad8e24cfb..a853395a6 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -33,9 +33,7 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -48,7 +46,7 @@ Module ZDivPropFunct (Import Z : ZDivSig).
   apply le_trans with 0; [ rewrite opp_nonpos_nonneg |]; order.
   Qed.
  End Z'.
- Module Import NZDivP := NZDivPropFunct Z'.
+ Module Import NZDivP := NZDivPropFunct Z' ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index fe695907d..551ce6b41 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -36,9 +36,7 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
@@ -47,7 +45,7 @@ Module ZDivPropFunct (Import Z : ZDivSig).
   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'.
+ Module Import NZDivP := NZDivPropFunct Z' ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index b57f8e27f..c60bf7c6a 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -37,13 +37,11 @@ End ZDiv.
 
 Module Type ZDivSig := ZAxiomsSig <+ ZDiv.
 
-Module ZDivPropFunct (Import Z : ZDivSig).
- (* TODO: en faire un arg du foncteur + comprendre le bug de SearchAbout *)
- Module Import ZP := ZPropFunct Z.
+Module ZDivPropFunct (Import Z : ZDivSig)(Import ZP : ZPropSig Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := NZDivPropFunct Z.
+ Module Import NZDivP := NZDivPropFunct Z ZP.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index a9cf0dc4d..bd9a85714 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -12,7 +12,7 @@
 
 Require Export ZAddOrder.
 
-Module ZMulOrderPropFunct (Import Z : ZAxiomsSig).
+Module Type ZMulOrderPropFunct (Import Z : ZAxiomsSig).
 Include ZAddOrderPropFunct Z.
 Local Open Scope NumScope.
 
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index eee5b0273..7f2253205 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -15,4 +15,9 @@ Require Export ZAxioms ZMulOrder.
     subsumes all others.
 *)
 
-Module ZPropFunct := ZMulOrderPropFunct.
+Module Type ZPropSig := ZMulOrderPropFunct.
+
+Module ZPropFunct (Z:ZAxiomsSig) <: ZPropSig Z.
+ Include Type ZPropSig Z.
+End ZPropFunct.
+