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, 32 insertions, 32 deletions

diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index fe66d88c6..aaf6bfc22 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -12,18 +12,18 @@ Require Import NZAxioms NZMulOrder.
 
 (** The first signatures will be common to all divisions over NZ, N and Z *)
 
-Module Type DivMod (Import T:Typ).
+Module Type DivMod (Import A : Typ).
  Parameters Inline div modulo : t -> t -> t.
 End DivMod.
 
-Module Type DivModNotation (T:Typ)(Import NZ:DivMod T).
+Module Type DivModNotation (A : Typ)(Import B : DivMod A).
  Infix "/" := div.
  Infix "mod" := modulo (at level 40, no associativity).
 End DivModNotation.
 
-Module Type DivMod' (T:Typ) := DivMod T <+ DivModNotation T.
+Module Type DivMod' (A : Typ) := DivMod A <+ DivModNotation A.
 
-Module Type NZDivCommon (Import NZ : NZAxiomsSig')(Import DM : DivMod' NZ).
+Module Type NZDivCommon (Import A : NZAxiomsSig')(Import B : DivMod' A).
  Declare Instance div_wd : Proper (eq==>eq==>eq) div.
  Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo.
  Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b).
@@ -36,19 +36,19 @@ End NZDivCommon.
     NB: This axiom would also be true for N and Z, but redundant.
 *)
 
-Module Type NZDivSpecific (Import NZ : NZOrdAxiomsSig')(Import DM : DivMod' NZ).
+Module Type NZDivSpecific (Import A : NZOrdAxiomsSig')(Import B : DivMod' A).
  Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b.
 End NZDivSpecific.
 
-Module Type NZDiv (NZ:NZOrdAxiomsSig)
- := DivMod NZ <+ NZDivCommon NZ <+ NZDivSpecific NZ.
+Module Type NZDiv (A : NZOrdAxiomsSig)
+ := DivMod A <+ NZDivCommon A <+ NZDivSpecific A.
 
-Module Type NZDiv' (NZ:NZOrdAxiomsSig) := NZDiv NZ <+ DivModNotation NZ.
+Module Type NZDiv' (A : NZOrdAxiomsSig) := NZDiv A <+ DivModNotation A.
 
-Module NZDivProp
- (Import NZ : NZOrdAxiomsSig')
- (Import NZP : NZMulOrderProp NZ)
- (Import NZD : NZDiv' NZ).
+Module Type NZDivProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZDiv' A)
+ (Import C : NZMulOrderProp A).
 
 (** Uniqueness theorems *)
 
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index a9b2fdc31..ea1f1bad6 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -12,31 +12,31 @@ Require Import NZAxioms NZMulOrder.
 
 (** Interface of a power function, then its specification on naturals *)
 
-Module Type Pow (Import T:Typ).
+Module Type Pow (Import A : Typ).
  Parameters Inline pow : t -> t -> t.
 End Pow.
 
-Module Type PowNotation (T:Typ)(Import NZ:Pow T).
+Module Type PowNotation (A : Typ)(Import B : Pow A).
  Infix "^" := pow.
 End PowNotation.
 
-Module Type Pow' (T:Typ) := Pow T <+ PowNotation T.
+Module Type Pow' (A : Typ) := Pow A <+ PowNotation A.
 
-Module Type NZPowSpec (Import NZ : NZOrdAxiomsSig')(Import P : Pow' NZ).
+Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A).
  Declare Instance pow_wd : Proper (eq==>eq==>eq) pow.
  Axiom pow_0_r : forall a, a^0 == 1.
  Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
 End NZPowSpec.
 
-Module Type NZPow (NZ:NZOrdAxiomsSig) := Pow NZ <+ NZPowSpec NZ.
-Module Type NZPow' (NZ:NZOrdAxiomsSig) := Pow' NZ <+ NZPowSpec NZ.
+Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A.
+Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A.
 
 (** Derived properties of power *)
 
-Module NZPowProp
- (Import NZ : NZOrdAxiomsSig')
- (Import NZP : NZMulOrderProp NZ)
- (Import NZP' : NZPow' NZ).
+Module Type NZPowProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZPow' A)
+ (Import C : NZMulOrderProp A).
 
 Hint Rewrite pow_0_r pow_succ_r : nz.
 
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 425e4d6b8..a40aa7657 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -12,30 +12,30 @@ Require Import NZAxioms NZMulOrder.
 
 (** Interface of a sqrt function, then its specification on naturals *)
 
-Module Type Sqrt (Import T:Typ).
+Module Type Sqrt (Import A : Typ).
  Parameters Inline sqrt : t -> t.
 End Sqrt.
 
-Module Type SqrtNotation (T:Typ)(Import NZ:Sqrt T).
+Module Type SqrtNotation (A : Typ)(Import B : Sqrt A).
  Notation "√ x" := (sqrt x) (at level 25).
 End SqrtNotation.
 
-Module Type Sqrt' (T:Typ) := Sqrt T <+ SqrtNotation T.
+Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.
 
-Module Type NZSqrtSpec (Import NZ : NZOrdAxiomsSig')(Import P : Sqrt' NZ).
+Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
  Declare Instance sqrt_wd : Proper (eq==>eq) sqrt.
  Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a).
 End NZSqrtSpec.
 
-Module Type NZSqrt (NZ:NZOrdAxiomsSig) := Sqrt NZ <+ NZSqrtSpec NZ.
-Module Type NZSqrt' (NZ:NZOrdAxiomsSig) := Sqrt' NZ <+ NZSqrtSpec NZ.
+Module Type NZSqrt (A : NZOrdAxiomsSig) := Sqrt A <+ NZSqrtSpec A.
+Module Type NZSqrt' (A : NZOrdAxiomsSig) := Sqrt' A <+ NZSqrtSpec A.
 
 (** Derived properties of power *)
 
-Module NZSqrtProp
- (Import NZ : NZOrdAxiomsSig')
- (Import NZP' : NZSqrt' NZ)
- (Import NZP : NZMulOrderProp NZ).
+Module Type NZSqrtProp
+ (Import A : NZOrdAxiomsSig')
+ (Import B : NZSqrt' A)
+ (Import C : NZMulOrderProp A).
 
 (** First, sqrt is non-negative *)