Commit 94c0f0db authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 3643ac1d
Pipeline #40939 passed with stage
in 17 minutes and 59 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iris-c" ]
depends: [
"coq-iris-heap-lang" { (= "dev.2020-12-04.7.68955c65") | (= "dev") }
"coq-iris-heap-lang" { (= "dev.2021-01-25.1.21b7ffa1") | (= "dev") }
]
......@@ -49,13 +49,13 @@ Proof.
apply lvl_included. destruct lv1, lv2; compute; firstorder.
Qed.
Canonical Structure lvlR : cmraT := discreteR lvl lvl_ra_mixin.
Canonical Structure lvlR : cmra := discreteR lvl lvl_ra_mixin.
Global Instance lvl_cmra_discrete : CmraDiscrete lvlR.
Proof. apply discrete_cmra_discrete. Qed.
Lemma lvl_ucmra_mixin : UcmraMixin lvl.
Proof. split; try (apply _ || done). by intros []. Qed.
Canonical Structure lvlUR : ucmraT := UcmraT lvl lvl_ucmra_mixin.
Canonical Structure lvlUR : ucmra := Ucmra lvl lvl_ucmra_mixin.
(** Here we use a Primitive Record to get an eta-rule for cloc
See: https://coq.inria.fr/refman/language/gallina-extensions.html#primitive-record-types
......@@ -81,9 +81,9 @@ Instance cloc_inhabited : Inhabited cloc | 0 :=
populate (CLoc inhabitant inhabitant).
(* Auth (CLoc -> (Q * Level)) *)
Definition locking_heapUR : ucmraT :=
Definition locking_heapUR : ucmra :=
gmapUR cloc (prodR (prodR fracR lvlUR) (agreeR valO)).
Definition heap_block_infoUR : ucmraT :=
Definition heap_block_infoUR : ucmra :=
gmapUR loc (agreeR (prodO boolO natO)).
(** The CMRA we need. *)
......
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