Commit bcfe1b36 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris and get rid of some annotations.

parent 015c416f
Pipeline #4507 passed with stage
in 24 minutes and 59 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
depends: [
"coq-iris" { (= "dev.2017-09-21.1") | (= "dev") }
"coq-iris" { (= "dev.2017-09-21.3") | (= "dev") }
]
......@@ -281,8 +281,7 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
pose s'' := state_hist_update h' s'.
iMod ("HClose" $! s'' (: sts.tokens rsl_sts)
with "[Itpr ItprD Inv Hist]") as "(Inv & #Own)".
iMod ("HClose" $! s'' with "[Itpr ItprD Inv Hist]") as "(Inv & #Own)".
{ iSplitL "".
- iPureIntro. by apply (state_hist_update_steps _ v V').
- rewrite /rsl_inv. iNext.
......@@ -582,7 +581,7 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
as (i) "[% #Hi]".
destruct (frame_steps_RMW_branch _ _ _ H _ _ H0) as [I' [h' Eq]].
iMod ("SClose" $! (state_ISet_insert i s') ({[Change i]} : sts.tokens rsl_sts)
iMod ("SClose" $! (state_ISet_insert i s') {[Change i]}
with "[Inv]") as "(Inv & Own')".
{ iSplitL "".
- iPureIntro. by apply state_ISet_insert_steps.
......@@ -1442,8 +1441,7 @@ Instance InitRaw_persistent V jγ : PersistentP (InitRaw V jγ) := _.
by eapply frame_steps_steps. }
iMod ("HClose2" $! s'' ({[Change i1; Change i2]} : sts.tokens rsl_sts) with "[Inv]")
as "(Inv & Own)".
iMod ("HClose2" $! s'' {[Change i1; Change i2]} with "[Inv]") as "(Inv & Own)".
{ iSplitL "".
- iPureIntro. by apply state_ISet_split_steps.
- iNext.
......
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