2 files changed, 6 insertions, 3 deletions
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index f15ab222ce..d6fc88338c 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -13,11 +13,12 @@
  left projection. *)
 
 Require Import FMapInterface.
+Import Morphisms. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (X:OrderedType).
+Module Raw (Import X:OrderedType).
 
 Module Import MX := OrderedTypeFacts X.
 Module Import PX := KeyOrderedType X.
@@ -1154,7 +1155,7 @@ Section Elt.
 
 End Make.
 
-Module Make_ord (X: OrderedType)(D : OrderedType) <:
+Module Make_ord (X: OrderedType)(Import D : OrderedType) <:
 Sord with Module Data := D
         with Module MapS.E := X.
 
@@ -1332,6 +1333,7 @@ Proof.
   inversion_clear Hm2; auto.
  destruct (IHm1 Hm11 (Build_slist Hm22));
   [ apply LT | apply EQ | apply GT ]; cmp_solve.
+Show.
 Qed.
 
 End Make_ord.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 6c1e8ca89b..a952d56798 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -12,11 +12,12 @@
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
 Require Import FMapInterface.
+Import Morphisms_Prop. (* For Hints *)
 
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Module Raw (X:DecidableType).
+Module Raw (Import X:DecidableType).
 
 Module Import PX := KeyDecidableType X.