3 files changed, 4 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 954b89150a..fe951a7511 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -43,7 +43,7 @@ Module ZEuclidProp
  (Import C : ZSgnAbsProp A B)
  (Import D : ZEuclid' A).
 
- Module Import NZDivP := Nop <+ NZDivProp A D B.
+ Module Import Private_NZDiv := Nop <+ NZDivProp A D B.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivFloor.v b/theories/Numbers/Integer/Abstract/ZDivFloor.v
index 0e54c453b7..14003d8926 100644
--- a/theories/Numbers/Integer/Abstract/ZDivFloor.v
+++ b/theories/Numbers/Integer/Abstract/ZDivFloor.v
@@ -32,7 +32,7 @@ Module Type ZDivProp
  (Import C : ZSgnAbsProp A B).
 
 (** We benefit from what already exists for NZ *)
-Module Import NZDivP := Nop <+ NZDivProp A A B.
+Module Import Private_NZDiv := Nop <+ NZDivProp A A B.
 
 (** Another formulation of the main equation *)
 
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 74abedb423..bd8b6ce239 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -33,6 +33,7 @@ Module Type ZQuotProp
 
 (** We benefit from what already exists for NZ *)
 
+ Module Import Private_Div.
  Module Quot2Div <: NZDiv A.
   Definition div := quot.
   Definition modulo := A.rem.
@@ -41,8 +42,8 @@ Module Type ZQuotProp
   Definition div_mod := quot_rem.
   Definition mod_bound_pos := rem_bound_pos.
  End Quot2Div.
-
  Module NZQuot := Nop <+ NZDivProp A Quot2Div B.
+ End Private_Div.
 
 Ltac pos_or_neg a :=
  let LT := fresh "LT" in