From 9fddc01a8dadffb64c9e01396e7bf3bc28270966 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 2 May 2023 13:58:32 +0200 Subject: [PATCH] Set `Hint Mode` for `Equiv`. --- stdpp/base.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/stdpp/base.v b/stdpp/base.v index 52068077..9eda10f5 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 -- GitLab