Commit 8e3d7431 authored by Robbert Krebbers's avatar Robbert Krebbers

Bump Iris.

parent 7b03d0b3
Pipeline #20243 passed with stage
in 17 minutes and 5 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-09-19.0.ca3f9d11") | (= "dev") }
"coq-iris" { (= "dev.2019-09-19.3.aa7871c7") | (= "dev") }
]
......@@ -501,7 +501,7 @@ Section properties.
Lemma alloc_heap_lookup σ l vs (i j : nat) :
( i, σ !! CLoc l i = None)
alloc_heap σ l vs j !! CLoc l (j + i) = ((ULvl,) <$> vs) !! i.
alloc_heap σ l vs j !! CLoc l (j + i) = ((ULvl,.) <$> vs) !! i.
Proof.
intros Hσi. revert i j. induction vs as [|v vs IH]=> i j; csimpl.
{ by rewrite Hσi. }
......@@ -567,7 +567,7 @@ Section properties.
(alloc_singleton_local_update _ l (to_agree (k, length vs)))=> //.
by rewrite /to_heap_block_info lookup_fmap Hτi. }
iModIntro. iSplit; first done. iSplitL "Hσ H Hτ Hll".
{ iExists (<[l:=ActiveBlock k ((ULvl,) <$> vs)]> τ). iFrame "Hσ". iSplit.
{ iExists (<[l:=ActiveBlock k ((ULvl,.) <$> vs)]> τ). iFrame "Hσ". iSplit.
{ iPureIntro. split.
{ clear -Hnat. generalize 0. induction vs as [|v vs IH]=> j //=.
apply map_Forall_insert_2; simpl; eauto with lia. }
......
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