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/MSetList.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/MSetList.v')
| -rw-r--r-- | theories/MSets/MSetList.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v index c5e300cdd..4292eb938 100644 --- a/theories/MSets/MSetList.v +++ b/theories/MSets/MSetList.v @@ -218,6 +218,11 @@ Module MakeRaw (X: OrderedType) <: RawSets X. Notation Inf := (lelistA X.lt). 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 := Sort. Class Ok (s:t) : Prop := { ok : Sort s }. |