diff --git a/src/Util/FSets/FMapFlip.v b/src/Util/FSets/FMapFlip.v
index a981feb501..1e516e7ea1 100644
--- a/src/Util/FSets/FMapFlip.v
+++ b/src/Util/FSets/FMapFlip.v
@@ -31,6 +31,9 @@ Local Set Keyed Unification.
 
 Module FlipWSfun (E : DecidableTypeOrig) (W' : WSfun E) <: WSfun E.
   Module E' := E <+ UpdateEq.
+  Global Remove Hints E'.eq_refl E'.eq_sym E'.eq_trans : core.
+  Local Hint Resolve E'.eq_refl E'.eq_sym E'.eq_trans : core.
+
   Local Instance W'_eq_key_equiv elt : Equivalence (@W'.eq_key elt) | 10. split; cbv; eauto. Qed.
   Local Instance W'_eq_key_elt_equiv elt : Equivalence (@W'.eq_key_elt elt) | 10. split; repeat intros [? ?]; cbv in *; subst; eauto. Qed.
 
@@ -124,6 +127,7 @@ End FlipWSfun.
 
 Module FlipWeakMap (W' : WS) <: WS.
   Module E := W'.E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
   Include FlipWSfun W'.E W'.
 End FlipWeakMap.
 
@@ -146,11 +150,13 @@ End FlipSfun.
 
 Module FlipUsualMap (S' : UsualS) <: UsualS.
   Module E <: UsualOrderedTypeOrig := FlipUsualOrderedTypeOrig S'.E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
   Include FlipSfun S'.E S'.
 End FlipUsualMap.
 
 Module FlipMap (S' : S) <: S.
   Module E <: OrderedTypeOrig := FlipOrderedTypeOrig S'.E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
   Include FlipSfun S'.E S'.
 End FlipMap.
 
diff --git a/src/Util/FSets/FMapIso.v b/src/Util/FSets/FMapIso.v
index f187a84d11..e5932fb1b3 100644
--- a/src/Util/FSets/FMapIso.v
+++ b/src/Util/FSets/FMapIso.v
@@ -491,6 +491,7 @@ End IsoWSfun.
 
 Module IsoWS (W' : WS) (E : IsoDecidableTypeOrig W'.E) <: WS.
   Module E := E.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
   Include IsoWSfun W'.E W' E.
 End IsoWS.
 
@@ -515,6 +516,7 @@ End IsoSfun.
 
 Module IsoS (S' : S) (E' : IsoMiniOrderedType S'.E) <: S.
   Module E <: IsoOrderedTypeOrig S'.E := E' <+ OT_of_MOT.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
   Include IsoSfun S'.E S' E.
 End IsoS.
 
diff --git a/src/Util/FSets/FMapOption.v b/src/Util/FSets/FMapOption.v
index 6a9a9978bf..69eb2ddaf7 100644
--- a/src/Util/FSets/FMapOption.v
+++ b/src/Util/FSets/FMapOption.v
@@ -45,9 +45,14 @@ Module OptionWSfun_gen (E2 : DecidableTypeOrig) (M2 : WSfun E2).
   End ESigCompat.
   Module E1 <: DecidableTypeBoth := UnitDecidableTypeBoth.
   Module E2 <: DecidableTypeBoth := E2 <+ UpdateEq.
+  Global Remove Hints E2.eq_refl E2.eq_sym E2.eq_trans : core.
   Module M1 <: WSfun E1 := UnitMap.
   Module OptionWSfun_gen (E : ESig) (ECompat : ESigCompat E) <: WSfun E.
     Module E' <: DecidableTypeBoth := E <+ UpdateEq <+ ECompat.
+    Global Remove Hints E'.eq_refl E'.eq_sym E'.eq_trans : core.
+    Local Hint Resolve E2.eq_refl E2.eq_sym E2.eq_trans : core.
+    Local Hint Resolve E.eq_refl E.eq_sym E.eq_trans : core.
+
     Local Instance M1_eq_key_equiv elt : Equivalence (@M1.eq_key elt) | 10. split; cbv; repeat intro; destruct_head'_prod; destruct_head'_unit; eauto. Qed.
     Local Instance M1_eq_key_elt_equiv elt : Equivalence (@M1.eq_key_elt elt) | 10. split; repeat intros [? ?]; cbv in *; subst; eauto. Qed.
     Local Instance M2_eq_key_equiv elt : Equivalence (@M2.eq_key elt) | 10. split; cbv; eauto. Qed.
diff --git a/src/Util/FSets/FMapProd.v b/src/Util/FSets/FMapProd.v
index a190d85018..4abf869634 100644
--- a/src/Util/FSets/FMapProd.v
+++ b/src/Util/FSets/FMapProd.v
@@ -44,9 +44,16 @@ Module ProdWSfun_gen (E1 : DecidableTypeOrig) (E2 : DecidableTypeOrig) (M1 : WSf
     Axiom eq_alt : forall x y, E.eq x y <-> RelProd E1.eq E2.eq x y.
   End ESigCompat.
   Module E1 <: DecidableTypeBoth := E1 <+ UpdateEq.
+  Global Remove Hints E1.eq_refl E1.eq_sym E1.eq_trans : core.
   Module E2 <: DecidableTypeBoth := E2 <+ UpdateEq.
+  Global Remove Hints E2.eq_refl E2.eq_sym E2.eq_trans : core.
   Module ProdWSfun_gen (E : ESig) (ECompat : ESigCompat E) <: WSfun E.
     Module E' <: DecidableTypeBoth := E <+ UpdateEq <+ ECompat.
+    Global Remove Hints E'.eq_refl E'.eq_sym E'.eq_trans : core.
+    Local Hint Resolve E1.eq_refl E1.eq_sym E1.eq_trans
+          E2.eq_refl E2.eq_sym E2.eq_trans
+          E'.eq_refl E'.eq_sym E'.eq_trans
+      : core.
     Local Instance M1_eq_key_equiv elt : Equivalence (@M1.eq_key elt) | 10. split; cbv; eauto. Qed.
     Local Instance M1_eq_key_elt_equiv elt : Equivalence (@M1.eq_key_elt elt) | 10. split; repeat intros [? ?]; cbv in *; subst; eauto. Qed.
     Local Instance M2_eq_key_equiv elt : Equivalence (@M2.eq_key elt) | 10. split; cbv; eauto. Qed.
@@ -1158,8 +1165,13 @@ Module ProdSfun_gen (E1 : OrderedTypeOrig) (E2 : OrderedTypeOrig) (M1 : Sfun E1)
   Module ProdSfun_gen (E : ESig) (ECompat : ESigCompat E) <: Sfun E.
     Include ProdWSfun.ProdWSfun_gen E ECompat.
     Module E1' := E1 <+ UpdateStrOrder.
+    Global Remove Hints E1'.eq_refl E1'.eq_sym E1'.eq_trans : core.
     Module E2' := E2 <+ UpdateStrOrder.
+    Global Remove Hints E2'.eq_refl E2'.eq_sym E2'.eq_trans : core.
     Local Existing Instances eq_key_equiv eq_key_elt_equiv.
+    Local Hint Resolve E1'.eq_refl E1'.eq_sym E1'.eq_trans
+          E2'.eq_refl E2'.eq_sym E2'.eq_trans
+      : core.
     Section elt.
       Variable elt:Type.
       Definition lt_key (p p':key*elt) := E.lt (fst p) (fst p').
diff --git a/src/Util/FSets/FMapSect.v b/src/Util/FSets/FMapSect.v
index 0750cb20d8..3bdfabc0fe 100644
--- a/src/Util/FSets/FMapSect.v
+++ b/src/Util/FSets/FMapSect.v
@@ -713,6 +713,7 @@ End SectSfun.
 
 Module SectS (S' : S) (E' : SectMiniOrderedType S'.E) <: S.
   Module E <: SectOrderedTypeOrig S'.E := E' <+ OT_of_MOT.
+  Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
   Include SectSfun S'.E S' E.
 End SectS.
 
diff --git a/src/Util/FSets/FMapSum.v b/src/Util/FSets/FMapSum.v
index cbac7aa180..d558c76d58 100644
--- a/src/Util/FSets/FMapSum.v
+++ b/src/Util/FSets/FMapSum.v
@@ -42,9 +42,16 @@ Module SumWSfun_gen (E1 : DecidableTypeOrig) (E2 : DecidableTypeOrig) (M1 : WSfu
     Axiom eq_alt : forall x y, E.eq x y <-> sumwise E1.eq E2.eq x y.
   End ESigCompat.
   Module E1 <: DecidableTypeBoth := E1 <+ UpdateEq.
+  Global Remove Hints E1.eq_refl E1.eq_sym E1.eq_trans : core.
   Module E2 <: DecidableTypeBoth := E2 <+ UpdateEq.
+  Global Remove Hints E2.eq_refl E2.eq_sym E2.eq_trans : core.
   Module SumWSfun_gen (E : ESig) (ECompat : ESigCompat E) <: WSfun E.
     Module E' <: DecidableTypeBoth := E <+ UpdateEq <+ ECompat.
+    Global Remove Hints E.eq_refl E.eq_sym E.eq_trans : core.
+    Local Hint Resolve E1.eq_refl E1.eq_sym E1.eq_trans
+          E2.eq_refl E2.eq_sym E2.eq_trans
+          E.eq_refl E.eq_sym E.eq_trans
+      : core.
     Local Instance M1_eq_key_equiv elt : Equivalence (@M1.eq_key elt) | 10. split; cbv; eauto. Qed.
     Local Instance M1_eq_key_elt_equiv elt : Equivalence (@M1.eq_key_elt elt) | 10. split; repeat intros [? ?]; cbv in *; subst; eauto. Qed.
     Local Instance M2_eq_key_equiv elt : Equivalence (@M2.eq_key elt) | 10. split; cbv; eauto. Qed.
diff --git a/src/Util/FSets/FMapTrie.v b/src/Util/FSets/FMapTrie.v
index cd861bd3c2..7926c30e59 100644
--- a/src/Util/FSets/FMapTrie.v
+++ b/src/Util/FSets/FMapTrie.v
@@ -60,8 +60,13 @@ Module ListWSfun_gen (Y : DecidableTypeOrig) (M : WSfun Y) (Import T : Trie Y M)
     Axiom eq_alt : forall x y, E.eq x y <-> eqlistA Y.eq x y.
   End ESigCompat.
   Module Y' <: DecidableTypeBoth := Y <+ UpdateEq.
+  Global Remove Hints Y'.eq_refl Y'.eq_sym Y'.eq_trans : core.
   Module ListWSfun_gen (E : ESig) (ECompat : ESigCompat E) <: WSfun E.
     Module E' <: DecidableTypeBoth := E <+ UpdateEq <+ ECompat.
+    Global Remove Hints E'.eq_refl E'.eq_sym E'.eq_trans : core.
+    Local Hint Resolve Y'.eq_refl Y'.eq_sym Y'.eq_trans
+          E'.eq_refl E'.eq_sym E'.eq_trans
+      : core.
     Local Instance M_eq_key_equiv elt : Equivalence (@M.eq_key elt) | 10. split; cbv; eauto. Qed.
     Local Instance M_eq_key_elt_equiv elt : Equivalence (@M.eq_key_elt elt) | 10. split; repeat intros [? ?]; cbv in *; subst; eauto. Qed.
 
@@ -1731,6 +1736,7 @@ Module ListSfun_gen (Y : OrderedTypeOrig) (M : Sfun Y) (Import T : Trie Y M).
   Module ListSfun_gen (E : ESig) (ECompat : ESigCompat E) <: Sfun E.
     Include ListWSfun.ListWSfun_gen E ECompat.
     Module Y' := Y <+ UpdateEq <+ UpdateStrOrder.
+    Global Remove Hints Y'.eq_refl Y'.eq_sym Y'.eq_trans : core.
     Module P' := ListStrOrder Y'.
     Local Existing Instances eq_key_equiv eq_key_elt_equiv.
     Local Instance M_lt_key_Transitive elt' : Transitive (@M.lt_key elt') | 10.