Commit 9b841f5e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Update to latest Iris.

This fixes issue #1.
parent 6e5908c3
Pipeline #4996 passed with stage
in 3 minutes and 23 seconds
...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"] ...@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"] install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"] remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [ depends: [
"coq-iris" { (= "dev.2017-10-19.0") | (= "dev") } "coq-iris" { (= "dev.2017-10-28.0") | (= "dev") }
] ]
...@@ -49,7 +49,7 @@ Definition recv (l : loc) (R : iProp Σ) : iProp Σ := ...@@ -49,7 +49,7 @@ Definition recv (l : loc) (R : iProp Σ) : iProp Σ :=
saved_prop_own i Q (Q - R))%I. saved_prop_own i Q (Q - R))%I.
Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) : Global Instance barrier_ctx_persistent (γ : gname) (l : loc) (P : iProp Σ) :
PersistentP (barrier_ctx γ l P). Persistent (barrier_ctx γ l P).
Proof. apply _. Qed. Proof. apply _. Qed.
(** Setoids *) (** Setoids *)
......
...@@ -24,7 +24,7 @@ Definition tok (s : state) : set token := ...@@ -24,7 +24,7 @@ Definition tok (s : state) : set token :=
(if state_phase s is High then {[ Send ]} else ). (if state_phase s is High then {[ Send ]} else ).
Global Arguments tok !_ /. Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prim_step tok. Canonical Structure sts := sts.Sts prim_step tok.
(* The set of states containing some particular i *) (* The set of states containing some particular i *)
Definition i_states (i : gname) : set state := {[ s | i state_I s ]}. Definition i_states (i : gname) : set state := {[ s | i state_I s ]}.
......
Markdown is supported
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