From 309a7a572a0cc47588212e622f062d2ab629b15e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <6797-mattam82@users.noreply.gitlab.mpi-sws.org>
Date: Tue, 11 Jan 2022 15:35:11 +0000
Subject: [PATCH] Declare `equiv` as a rightful rewrite relation, when an
 `Equiv` instance is available.

---
 theories/base.v | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/theories/base.v b/theories/base.v
index 029b7fa4..b94fa2f5 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -250,6 +250,13 @@ Class Equiv A := equiv: relation A.
 (* No Hint Mode set because of Coq bug #14441.
 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]. *)
+Global Instance equiv_rewrite_relation `{Equiv A} :
+  RewriteRelation (@equiv A _) := {}.   
+
 Infix "≡" := equiv (at level 70, no associativity) : stdpp_scope.
 Infix "≡@{ A }" := (@equiv A _)
   (at level 70, only parsing, no associativity) : stdpp_scope.
-- 
GitLab