11 files changed, 57 insertions, 45 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,
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 *)
 
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index be56c8b03..0bb66ab2f 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 0039a1e2c..8ab460a2f 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 d5916bdc2..92e90b9c8 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'.
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 0a6dba982..14d34f1eb 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -11,6 +11,12 @@ Require Export RelationClasses.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** Structure with nothing inside.
+    Used to force a module type T into a module via Nop <+ T. (HACK!) *)
+
+Module Type Nop.
+End Nop.
+
 (** * Structure with just a base type [t] *)
 
 Module Type Typ.