Commit 638eac93 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris (C→O rename).

parent 424e57c6
Pipeline #17888 passed with stage
in 2 minutes and 47 seconds
......@@ -58,12 +58,12 @@ Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the
proofs, we now need to make sure that we can use integer ghost variables. For
this, we add the type class constraint:
inG Σ (authR (optionUR (exclR ZC)))
inG Σ (authR (optionUR (exclR ZO)))
*)
Section proof2.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZC)))}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZO)))}.
Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ :=
( n1 n2 : Z, r #(n1 + n2)
......
......@@ -26,7 +26,7 @@ Definition parallel_add_mul : expr :=
(** In this proof we will make use of Boolean ghost variables. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolC)))}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolO)))}.
(** The same helping lemmas for ghost variables that we have already seen in
the previous exercise. *)
......
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [] # This repo does not install
remove: []
depends: [
"coq-iris" { (= "dev.2019-06-11.8.a51fa3cf") | (= "dev") }
"coq-iris" { (= "dev.2019-06-18.2.e039d7c7") | (= "dev") }
]
......@@ -62,12 +62,12 @@ Whereas we previously abstracted over an arbitrary "ghost state" [Σ] in the
proofs, we now need to make sure that we can use integer ghost variables. For
this, we add the type class constraint:
inG Σ (authR (optionUR (exclR ZC)))
inG Σ (authR (optionUR (exclR ZO)))
*)
Section proof2.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZC)))}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR ZO)))}.
Definition parallel_add_inv_2 (r : loc) (γ1 γ2 : gname) : iProp Σ :=
( n1 n2 : Z, r #(n1 + n2)
......
......@@ -26,7 +26,7 @@ Definition parallel_add_mul : expr :=
(** In this proof we will make use of Boolean ghost variables. *)
Section proof.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolC)))}.
Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolO)))}.
(** The same helping lemmas for ghost variables that we have already seen in
the previous exercise. *)
......
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