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

1 files changed, 12 insertions, 12 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 *)