From a9140f8ed71c85874c789a297e1a657a0818ff1c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <6797-mattam82@users.noreply.gitlab.mpi-sws.org>
Date: Fri, 14 Jan 2022 11:26:28 +0000
Subject: [PATCH] Fix bi_rewrite_relation hint priority

---
 coq-iris.opam          | 2 +-
 iris/algebra/updates.v | 5 ++++-
 iris/bi/interface.v    | 6 +++++-
 3 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/coq-iris.opam b/coq-iris.opam
index a6da172a1..db729d188 100644
--- a/coq-iris.opam
+++ b/coq-iris.opam
@@ -28,7 +28,7 @@ tags: [
 
 depends: [
   "coq" { (>= "8.13" & < "8.16~") | (= "dev") }
-  "coq-stdpp" { (= "dev.2022-01-13.0.607ee2b1") | (= "dev") }
+  "coq-stdpp" { (= "dev.2022-01-14.1.ac02dbbd") | (= "dev") }
 ]
 
 build: ["./make-package" "iris" "-j%{jobs}%"]
diff --git a/iris/algebra/updates.v b/iris/algebra/updates.v
index 0d1b2a7fc..f5e61a3c1 100644
--- a/iris/algebra/updates.v
+++ b/iris/algebra/updates.v
@@ -52,8 +52,11 @@ Lemma cmra_update_exclusive `{!Exclusive x} y:
 Proof. move=>??[z|]=>[/exclusiveN_l[]|_]. by apply cmra_valid_validN. Qed.
 
 (** Updates form a preorder. *)
+(** We set this rewrite relation's priority below the stdlib's 
+  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
+  [eq] (at 100) < [≡] (at 150) < [cmra_update] (at 170) < [⊑] (at 200) *)
 Global Instance cmra_update_rewrite_relation :
-  RewriteRelation (@cmra_update A) := {}.
+  RewriteRelation (@cmra_update A) | 170 := {}.
 Global Instance cmra_update_preorder : PreOrder (@cmra_update A).
 Proof.
   split.
diff --git a/iris/bi/interface.v b/iris/bi/interface.v
index 3317c511c..90ec924a2 100644
--- a/iris/bi/interface.v
+++ b/iris/bi/interface.v
@@ -224,7 +224,11 @@ Global Arguments bi_persistently {PROP} _ : simpl never, rename.
 Global Arguments bi_later {PROP} _ : simpl never, rename.
 
 Global Hint Extern 0 (bi_entails _ _) => reflexivity : core.
-Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) := {}.
+(** We set this rewrite relation's priority below the stdlib's 
+  ([impl], [iff], [eq], ...) and [≡] but above [⊑].
+  [eq] (at 100) < [≡] (at 150) < [bi_entails _] (at 170) < [⊑] (at 200)
+*)
+Global Instance bi_rewrite_relation (PROP : bi) : RewriteRelation (@bi_entails PROP) | 170 := {}.
 Global Instance bi_inhabited {PROP : bi} : Inhabited PROP := populate (bi_pure True).
 
 Notation "P ⊢ Q" := (bi_entails P%I Q%I) : stdpp_scope.
-- 
GitLab