Merge branch 'pr-13969-take3' into 'master'

Fix bi_rewrite_relation hint priority

See merge request iris/iris!773

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}%"]

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.

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.