Skip to content

Commit

Permalink
Remove stupid hints from core db
Browse files Browse the repository at this point in the history
  • Loading branch information
JasonGross committed Jun 3, 2022
1 parent f9964a0 commit 3b7dbdc
Showing 1 changed file with 6 additions and 0 deletions.
6 changes: 6 additions & 0 deletions src/Util/FSets/FMapFlip.v
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down Expand Up @@ -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.

Expand All @@ -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.

Expand Down

0 comments on commit 3b7dbdc

Please sign in to comment.