5 files changed, 5 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).
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index f26f56d0c5..249674f3e6 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -11,6 +11,7 @@
 Require Export Decidable.
 Require Export NAxioms.
 Require Import NZProperties.
+Import Morphisms_Prop. (* For Hints *)
 
 Module NBasePropFunct (Import N : NAxiomsSig').
 (** First, we import all known facts about both natural numbers and integers. *)