Commit a9140f8e authored by Matthieu Sozeau's avatar Matthieu Sozeau Committed by Robbert Krebbers
Browse files

Fix bi_rewrite_relation hint priority

parent 5070f7f5
......@@ -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}%"]
......
......@@ -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.
......
......@@ -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.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment