4 files changed, 4 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 9f587a1d08..321c9eb89f 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 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 1f6c615bc3..79c95ded60 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -9,6 +9,7 @@
 (** 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 acc43fc179..6aa09dd546 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -10,6 +10,7 @@
 
 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 bfbcc2c65c..dc62b17176 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -9,6 +9,7 @@
 (************************************************************************)
 
 Require Import NZAxioms NZBase Decidable OrdersTac.
+Import Morphisms_Prop. (* For Hints *)
 
 Module Type NZOrderPropSig
  (Import NZ : NZOrdSig')(Import NZBase : NZBasePropSig NZ).