diff --git a/theories/base.v b/theories/base.v index 5ff6bee7b664e8a6994c05bfef095afa943ffc9e..ddbf6334f62fb0822ed76810cbc2ad1b008a8ba3 100644 --- a/theories/base.v +++ b/theories/base.v @@ -209,9 +209,9 @@ Instance: Params (@equiv) 2. (for types that have an [Equiv] instance) rather than the standard Leibniz equality. *) Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3. -Hint Extern 0 (_ ≡ _) => reflexivity. +Hint Extern 0 (?x ≡ ?y) => reflexivity. Hint Extern 0 (_ ≡ _) => symmetry; assumption. -Hint Extern 0 (_ ≡{_} _) => reflexivity. +Hint Extern 0 (?x ≡{_} ?y) => reflexivity. Hint Extern 0 (_ ≡{_} _) => symmetry; assumption. (** ** Operations on collections *)