From 00daaf86fc67b42d5df233a28b1ef11d33823abc Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <6797-mattam82@users.noreply.gitlab.mpi-sws.org>
Date: Thu, 13 Jan 2022 16:30:56 +0000
Subject: [PATCH] Set the priority of the rewrite relation for equiv to not
 take precedence over...

---
 theories/base.v | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index b94fa2f5..c4b2df78 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -252,10 +252,13 @@ 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 
-of shape  [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f] 
-when an equivalence relation is available on type [A]. *)
+of shape [Proper (eq ==> ?R) f] using [Proper (eq ==> (equiv (A:=A))) f]
+when an equivalence relation is available on type [A]. We put this instance
+at level 150 so it does not take precedence over Coq's stdlib instances,
+favoring inference of [eq] (all Coq functions are automatically morphisms
+for [eq]). *)
 Global Instance equiv_rewrite_relation `{Equiv A} :
-  RewriteRelation (@equiv A _) := {}.   
+  RewriteRelation (@equiv A _) | 150 := {}.
 
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
 Infix "≡@{ A }" := (@equiv A _)
-- 
GitLab