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

3 files changed, 9 insertions, 7 deletions

diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index be56c8b032..0bb66ab2f2 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -23,7 +23,7 @@ Module NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
   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 ND.
- Module Import NZDivP := NZDivProp N NP ND.
+ Module Import NZDivP := Nop <+ NZDivProp N ND NP.
 
  Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l.
 
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index 0039a1e2c8..8ab460a2f8 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -13,12 +13,14 @@ Require Import Bool NAxioms NSub NParity NZPow.
 (** Derived properties of power, specialized on natural numbers *)
 
 Module NPowProp
- (Import N : NAxiomsSig')(Import NS : NSubProp N)(Import NP : NParityProp N NS).
+ (Import A : NAxiomsSig')
+ (Import B : NSubProp A)
+ (Import C : NParityProp A B).
 
- Module Import NZPowP := NZPowProp N NS N.
+ Module Import NZPowP := Nop <+ NZPowProp A A B.
 
- Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
- Ltac wrap l := intros; apply l; auto'.
+Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
+Ltac wrap l := intros; apply l; auto'.
 
 Lemma pow_succ_r' : forall a b, a^(S b) == a * a^b.
 Proof. wrap pow_succ_r. Qed.
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index d5916bdc2d..92e90b9c80 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -10,9 +10,9 @@
 
 Require Import NAxioms NSub NZSqrt.
 
-Module NSqrtProp (Import N : NAxiomsSig')(Import NS : NSubProp N).
+Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A).
 
- Module Import NZSqrtP := NZSqrtProp N N NS.
+ Module Import NZSqrtP := Nop <+ NZSqrtProp A A B.
 
  Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
  Ltac wrap l := intros; apply l; auto'.