4 files changed, 6 insertions, 6 deletions
diff --git a/theories/Numbers/Natural/Abstract/NDiv.v b/theories/Numbers/Natural/Abstract/NDiv.v
index 1050516117..6db8e44895 100644
--- a/theories/Numbers/Natural/Abstract/NDiv.v
+++ b/theories/Numbers/Natural/Abstract/NDiv.v
@@ -13,7 +13,7 @@ Require Import NAxioms NSub NZDiv.
 Module Type NDivProp (Import N : NAxiomsSig')(Import NP : NSubProp N).
 
 (** We benefit from what already exists for NZ *)
-Module Import NZDivP := Nop <+ NZDivProp N N NP.
+Module Import Private_NZDiv := Nop <+ NZDivProp N N NP.
 
 Ltac auto' := try rewrite <- neq_0_lt_0; auto using le_0_l.
 
diff --git a/theories/Numbers/Natural/Abstract/NLog.v b/theories/Numbers/Natural/Abstract/NLog.v
index 0accf38b09..74827c6e76 100644
--- a/theories/Numbers/Natural/Abstract/NLog.v
+++ b/theories/Numbers/Natural/Abstract/NLog.v
@@ -18,6 +18,6 @@ Module Type NLog2Prop
 
  (** For the moment we simply reuse NZ properties *)
 
- Include NZLog2Prop A A A B D.NZPowP.
- Include NZLog2UpProp A A A B D.NZPowP.
+ Include NZLog2Prop A A A B D.Private_NZPow.
+ Include NZLog2UpProp A A A B D.Private_NZPow.
 End NLog2Prop.
diff --git a/theories/Numbers/Natural/Abstract/NPow.v b/theories/Numbers/Natural/Abstract/NPow.v
index b046e383dd..07aee9c6fb 100644
--- a/theories/Numbers/Natural/Abstract/NPow.v
+++ b/theories/Numbers/Natural/Abstract/NPow.v
@@ -17,7 +17,7 @@ Module Type NPowProp
  (Import B : NSubProp A)
  (Import C : NParityProp A B).
 
- Module Import NZPowP := Nop <+ NZPowProp A A B.
+ Module Import Private_NZPow := 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'.
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 1b49678e42..34b7d0110a 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -12,7 +12,7 @@ Require Import NAxioms NSub NZSqrt.
 
 Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A).
 
- Module Import NZSqrtP := Nop <+ NZSqrtProp A A B.
+ Module Import Private_NZSqrt := 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'.
@@ -70,6 +70,6 @@ Proof. wrap add_sqrt_le. Qed.
 
 (** For the moment, we include stuff about [sqrt_up] with patching them. *)
 
-Include NZSqrtUpProp A A B NZSqrtP.
+Include NZSqrtUpProp A A B Private_NZSqrt.
 
 End NSqrtProp.