Remove stupid hints from core db

Works around COQBUG(https://github.com/coq/coq/issues/16133)
JasonGross · Jun 3, 2022 · 0f37dd0 · 0f37dd0
1 parent 339292c
commit 0f37dd0
Show file tree

Hide file tree

Showing 6 changed files with 33 additions and 0 deletions.
diff --git 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
@@ -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
@@ -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
@@ -743,6 +743,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
@@ -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
@@ -59,8 +59,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.
 
@@ -1733,6 +1738,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.