Commit 05073110 authored by Dan Frumin's avatar Dan Frumin

Update for the new mset_member_spec

parent 6b1ce731
......@@ -77,7 +77,7 @@ Section proofs.
wp_let.
wp_apply wp_assert.
wp_apply (mset_member_spec #l env with "HX").
iIntros (w) "[Henv [[% %]|[% %]]]"; simplify_eq/=; first done.
iIntros "Henv /=". case_decide; first by exfalso. simpl.
wp_op. iSplit; eauto. iNext. wp_seq.
rewrite mapsto_eq /mapsto_def. iDestruct "Hv" as "[Hv Hl]". wp_load.
iCombine "Hv Hl" as "Hv".
......
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