8 files changed, 16 insertions, 13 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
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 3722d4727d..8cf5b26fb1 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -146,7 +146,8 @@ Definition lt_compat := lt_wd.
 Definition lt_total := lt_trichotomy.
 Definition le_lteq := lt_eq_cases.
 
-Module OrderElts <: TotalOrder.
+Module Private_OrderTac.
+Module Elts <: TotalOrder.
  Definition t := t.
  Definition eq := eq.
  Definition lt := lt.
@@ -156,9 +157,10 @@ Module OrderElts <: TotalOrder.
  Definition lt_compat := lt_compat.
  Definition lt_total := lt_total.
  Definition le_lteq := le_lteq.
-End OrderElts.
-Module OrderTac := !MakeOrderTac OrderElts.
-Ltac order := OrderTac.order.
+End Elts.
+Module Tac := !MakeOrderTac Elts.
+End Private_OrderTac.
+Ltac order := Private_OrderTac.Tac.order.
 
 (** Some direct consequences of [order]. *)
 
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.