Numbers: NZPowProp as a Module Type, some module variable renaming

  We temporary use a hack to convert a module type into a module
  Module M := T is refused, so we force an include via
  Module M := Nop <+ T where Nop is an empty module.
  To be fixed later more beautifully...

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

4 files changed, 10 insertions, 6 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index bb5c2410f..129785bad 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -49,7 +49,7 @@ Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
   apply mod_always_pos.
   Qed.
  End ZD.
- Module Import NZDivP := NZDivProp Z ZP ZD.
+ Module Import NZDivP := Nop <+ NZDivProp Z ZD ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index c619d8b07..fd962024c 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -50,7 +50,7 @@ Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
   Lemma mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
   Proof. intros. now apply mod_pos_bound. Qed.
  End ZD.
- Module Import NZDivP := NZDivProp Z ZP ZD.
+ Module Import NZDivP := Nop <+ NZDivProp Z ZD ZP.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 027223415..4ca692d00 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -42,7 +42,7 @@ Module ZDivProp (Import Z : ZDivSig')(Import ZP : ZProp Z).
 
 (** We benefit from what already exists for NZ *)
 
- Module Import NZDivP := NZDivProp Z ZP Z.
+ Module Import NZDivP := Nop <+ NZDivProp Z Z ZP.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 782a11024..0241c3476 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -10,9 +10,13 @@
 
 Require Import Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow.
 
-Module ZPowProp (Import Z : ZAxiomsSig')(Import ZM : ZMulOrderProp Z)
- (Import ZP : ZParityProp Z ZM)(Import ZS : ZSgnAbsProp Z ZM).
- Include NZPowProp Z ZM Z.
+Module Type ZPowProp
+ (Import A : ZAxiomsSig')
+ (Import B : ZMulOrderProp A)
+ (Import C : ZParityProp A B)
+ (Import D : ZSgnAbsProp A B).
+
+ Include NZPowProp A A B.
 
 (** Many results are directly the same as in NZPow, hence
     the Include above. We extend nonetheless a few of them,