From 4dd6ec099bcc02ce6840d498967579bafbe90d0d Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Fri, 14 Jan 2022 11:41:53 +0100
Subject: [PATCH] Leave more room for priorities between equiv and sqsubseteq

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

diff --git a/theories/base.v b/theories/base.v
index df6f2796..b5569123 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -256,7 +256,10 @@ 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]). *)
+for [eq]).
+  [eq] (at 100) < [≡] (at 150) < [⊑] (at 200).  
+
+*)
 Global Instance equiv_rewrite_relation `{Equiv A} :
   RewriteRelation (@equiv A _) | 150 := {}.
 
@@ -1359,8 +1362,10 @@ Notation "(.⊑ y )" := (λ x, sqsubseteq x y) (only parsing) : stdpp_scope.
 Infix "⊑@{ A }" := (@sqsubseteq A _) (at level 70, only parsing) : stdpp_scope.
 Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
-(** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv]. *)
-Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 160 := {}.
+(** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv].
+  [eq] (at 100) < [≡] (at 150) < [⊑] (at 200).  
+*)
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 200 := {}.
 
 Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
-- 
GitLab