diff options
Diffstat (limited to 'theories/Structures/DecidableType2.v')
| -rw-r--r-- | theories/Structures/DecidableType2.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Structures/DecidableType2.v b/theories/Structures/DecidableType2.v index 087a6a7dd..0957ef243 100644 --- a/theories/Structures/DecidableType2.v +++ b/theories/Structures/DecidableType2.v @@ -23,7 +23,7 @@ End BareEquality. (** * Specification of the equality by the Type Classe [Equivalence] *) Module Type IsEq (Import E:BareEquality). - Instance eq_equiv : Equivalence eq. + Declare Instance eq_equiv : Equivalence eq. Hint Resolve (@Equivalence_Reflexive _ _ eq_equiv). Hint Resolve (@Equivalence_Transitive _ _ eq_equiv). Hint Immediate (@Equivalence_Symmetric _ _ eq_equiv). |