Commit 1875cf7f authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

parents 9afa0407 af9bc4e4
......@@ -170,7 +170,7 @@ Section heap.
iFrame "Hmapsto". iIntros {h} "[% Hheap]". rewrite /heap_inv.
iApply (wp_load_pst _ (<[l:=v]>(of_heap h)));first by rewrite lookup_insert.
rewrite of_heap_singleton_op //. iFrame "Hheap". iNext.
iIntros "Hheap". iFrame "Hheap". iSplit; first by iPureIntro. done.
iIntros "$". by iSplit.
Qed.
Lemma wp_store N E l v' e v P Φ :
......
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