4 files changed, 0 insertions, 4 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 321c9eb89f..9f587a1d08 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 Require Import NZAxioms.
-Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZBasePropSig (Import NZ : NZDomainSig').
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 79c95ded60..1f6c615bc3 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -9,7 +9,6 @@
 (** Euclidean Division *)
 
 Require Import NZAxioms NZMulOrder.
-Import Morphisms_Prop. (* For Hints *)
 
 (** The first signatures will be common to all divisions over NZ, N and Z *)
 
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 6aa09dd546..acc43fc179 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -10,7 +10,6 @@
 
 Require Import NZAxioms.
 Require Import NZAddOrder.
-Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig').
 Include NZAddOrderPropSig NZ.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index dc62b17176..bfbcc2c65c 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 Require Import NZAxioms NZBase Decidable OrdersTac.
-Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZOrderPropSig
  (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ).