Commit f8cb4921 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 8bd17580
Pipeline #16811 failed with stage
in 6 minutes and 23 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" { (= "dev.2019-03-14.3.2d1c8352") | (= "dev") }
"coq-iris" { (= "dev.2019-05-01.1.c7164230") | (= "dev") }
]
......@@ -271,7 +271,7 @@ Section cwp_rules.
iIntros (γ env l I) "#Hlock Hres #Heq". wp_pures.
pose (I' := fmap (λ πR, ((πR.1/2)%Qp,πR.2)) I).
iAssert (flock_resources γ I' flock_resources γ I')%I with "[Hres]" as "[Hres1 Hres2]".
{ rewrite /flock_resources -big_sepM_sepM.
{ rewrite /flock_resources -big_sepM_sep.
rewrite /I' big_sepM_fmap /=.
iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl.
by rewrite -flock_res_op Qp_div_2. }
......@@ -285,7 +285,7 @@ Section cwp_rules.
- iNext. iIntros (w1 w2) "[[HΨ1 Hres1] [HΨ2 Hres2]]".
iAssert (flock_resources γ I)%I with "[Hres1 Hres2]" as "$".
{ iCombine "Hres1 Hres2" as "Hres".
rewrite /flock_resources -big_sepM_sepM.
rewrite /flock_resources -big_sepM_sep.
rewrite /I' big_sepM_fmap /=.
iApply (big_sepM_mono with "Hres"). iIntros (k x Hk). simpl.
by rewrite -flock_res_op Qp_div_2. }
......
......@@ -437,7 +437,7 @@ Section flock.
Proof.
iIntros (?). rewrite {1}/flocked.
iIntros "(Hst & Hfa & Htokens)".
rewrite !big_sepM_sepM.
rewrite !big_sepM_sep.
iDestruct "Htokens" as "(T2s & Hinvs & Hρs)".
rewrite /flocked.
iFrame "Hst Hfa".
......@@ -542,7 +542,7 @@ Section flock.
rewrite {1}/flocked /=.
iDestruct "H" as "(Hflkd & Hfactive & Hfa)".
do 2 rewrite big_sepM_sepM.
do 2 rewrite big_sepM_sep.
iDestruct "Hfa" as "(HT2s & #Hinvs & Hρs)".
iInv invN as ([|] fa fp)
......@@ -585,7 +585,7 @@ Section flock.
rewrite big_sepM_fmap. by iFrame. }
iApply (release_spec with "[$Hlk $Hlocked $Hunflkd]").
iModIntro. iNext. iIntros "_". iApply "HΦ".
rewrite /flock_res !big_sepM_sepM.
rewrite /flock_res !big_sepM_sep.
iFrame "Hρs Hinvs".
by iApply (big_sepM_own_frag with "Hemp").
Qed.
......@@ -631,7 +631,7 @@ Section flock.
by apply option_local_update, exclusive_local_update. }
iFrame "Hfactive".
rewrite /flock_res. rewrite !big_sepM_sepM.
rewrite /flock_res. rewrite !big_sepM_sep.
iDestruct "HRres" as "(HI & #Hinvs & Hρs)".
iFrame "Hinvs Hρ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