Commit 0d9e2d1b authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent b3159ec2
Pipeline #17185 passed with stage
in 9 minutes and 32 seconds
......@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
depends: [
"coq-iris" { (= "dev.2019-06-03.2.b368c861") | (= "dev") }
"coq-iris" { (= "dev.2019-06-04.2.322cdf37") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
......@@ -7,9 +7,9 @@ From iris_examples.barrier Require Import proof specification.
Set Default Proof Using "Type".
Definition one_shotR (Σ : gFunctors) (F : cFunctor) :=
csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ)).
csumR (exclR unitC) (agreeR $ laterC $ F (iPreProp Σ) _).
Definition Pending {Σ F} : one_shotR Σ F := Cinl (Excl ()).
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ)) : one_shotR Σ F :=
Definition Shot {Σ} {F : cFunctor} (x : F (iProp Σ) _) : one_shotR Σ F :=
Cinr $ to_agree $ Next $ cFunctor_map F (iProp_fold, iProp_unfold) x.
Class oneShotG (Σ : gFunctors) (F : cFunctor) :=
......@@ -28,7 +28,7 @@ Section proof.
Local Set Default Proof Using "Type*".
Context `{!heapG Σ, !barrierG Σ, !spawnG Σ, !oneShotG Σ F}.
Context (N : namespace).
Local Notation X := (F (iProp Σ)).
Local Notation X := (F (iProp Σ) _).
Definition barrier_res γ (Φ : X iProp Σ) : iProp Σ :=
( x, own γ (Shot x) Φ x)%I.
......
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