diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:38 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-05 15:24:38 +0000 |
| commit | 41138b8f14d17f3c409d592c18e5a4def664a2e8 (patch) | |
| tree | 53e61dcd72940f85a085c51d5dc579ffa84a0d86 /theories/MSets/MSetWeakList.v | |
| parent | f4ceaf2ce34c5cec168275dee3e7a99710bf835f (diff) | |
Avoid declaring hints about refl/sym/trans of eq in DecidableType2
This used to be convenient in FSets, but since we now try to integrate
DecidableType and OrderedType as foundation for other part of the stdlib,
this should be avoided, otherwise some eauto take a _long_ time.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/MSets/MSetWeakList.v')
| -rw-r--r-- | theories/MSets/MSetWeakList.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v index c49ab9d95..feab44f58 100644 --- a/theories/MSets/MSetWeakList.v +++ b/theories/MSets/MSetWeakList.v @@ -119,6 +119,11 @@ Module MakeRaw (X:DecidableType) <: WRawSets X. Notation NoDup := (NoDupA X.eq). Notation In := (InA X.eq). + (* TODO: modify proofs in order to avoid these hints *) + Hint Resolve (@Equivalence_Reflexive _ _ X.eq_equiv). + Hint Immediate (@Equivalence_Symmetric _ _ X.eq_equiv). + Hint Resolve (@Equivalence_Transitive _ _ X.eq_equiv). + Definition IsOk := NoDup. Class Ok (s:t) : Prop := { ok : NoDup s }. |