From 36bc5009d8c6ec24fd0b6e13fb37bb14765176b5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Fri, 14 Jan 2022 11:15:05 +0100
Subject: [PATCH] Fix sqsubseteq_rewrite's priority, making it lower than equiv

---
 theories/base.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index c4b2df78..df6f2796 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -1359,7 +1359,8 @@ 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.
 
-Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) := {}.
+(** [sqsubseteq] does not take precedence over the stdlib's instances or [equiv]. *)
+Global Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑@{A}) | 160 := {}.
 
 Global Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
-- 
GitLab