Skip to content
Snippets Groups Projects
Commit 73e3afad authored by Ralf Jung's avatar Ralf Jung
Browse files

update Iris, fix for _cofinite

parent 7030ac15
No related branches found
No related tags found
No related merge requests found
Pipeline #15266 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
opam
+ 1
− 1
View file @ 73e3afad
...@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"] ...@@ -9,6 +9,6 @@ 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.2019-03-05.0.38abc449") | (= "dev") } "coq-iris" { (= "dev.2019-03-06.2.f5d03e25") | (= "dev") }
"coq-autosubst" { = "dev.coq86" } "coq-autosubst" { = "dev.coq86" }
] ]
theories/barrier/proof.v
+ 2
− 2
View file @ 73e3afad
...@@ -165,8 +165,8 @@ Proof. ...@@ -165,8 +165,8 @@ Proof.
iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)". iIntros (?). iDestruct 1 as (γ P Q i) "(#Hsts & Hγ & #HQ & HQR)".
iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]") iMod (sts_openS (barrier_inv l P) _ _ γ with "[Hγ]")
as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto. as ([p I]) "(% & [Hl Hr] & Hclose)"; eauto.
iMod (saved_prop_alloc_strong I) as (i1) "[% #Hi1]". iMod (saved_prop_alloc_cofinite I) as (i1) "[% #Hi1]".
iMod (saved_prop_alloc_strong (I ∪ {[i1]})) iMod (saved_prop_alloc_cofinite (I ∪ {[i1]}))
as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2. as (i2) "[Hi2' #Hi2]"; iDestruct "Hi2'" as %Hi2.
rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2. rewrite ->not_elem_of_union, elem_of_singleton in Hi2; destruct Hi2.
iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]})) iMod ("Hclose" $! (State p ({[i1; i2]} ∪ I ∖ {[i]}))
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment