4 files changed, 10 insertions, 6 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index bb5c2410fa..129785bada 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 c619d8b07f..fd962024cc 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 0272234156..4ca692d007 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 782a110240..0241c34762 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,