diff --git a/stdpp/base.v b/stdpp/base.v index 52068077f8da11ce4ef9242fa8a1aa4c3cc8f25b..9eda10f5ee7bb32bb652d43c5083491704440ae1 100644 --- a/stdpp/base.v +++ b/stdpp/base.v @@ -265,8 +265,7 @@ Proof. split; repeat intro; congruence. Qed. "canonical" equivalence for a type. The typeclass is tied to the \equiv symbol. This is based on (Spitters/van der Weegen, 2011). *) Class Equiv A := equiv: relation A. -(* No Hint Mode set because of Coq bug #14441. -Global Hint Mode Equiv ! : typeclass_instances. *) +Global Hint Mode Equiv ! : typeclass_instances. (** We instruct setoid rewriting to infer [equiv] as a relation on type [A] when needed. This allows setoid_rewrite to solve constraints