diff options
Diffstat (limited to 'theories/MSets/MSetWeakList.v')
| -rw-r--r-- | theories/MSets/MSetWeakList.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index 2498d82889..8a5ba2d80f 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -123,14 +123,18 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv). Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv). Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv). + #[local] Hint Resolve eqr eqtrans : core. + #[local] Hint Immediate eqsym : core. Definition IsOk := NoDup. Class Ok (s:t) : Prop := ok : NoDup s. + #[local] Hint Unfold Ok : core. + #[local] Hint Resolve ok : core. Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }. |