Commit 40370710 authored by Robbert Krebbers's avatar Robbert Krebbers

Properly name variable.

parent 6567b894
......@@ -30,7 +30,7 @@ Section increment.
wp_apply load_spec.
(* Prove the atomic shift for load *)
iDestruct "AUpd" as (F P) "(HF & HP & #AShft)".
iExists F, P. iFrame. iIntros "!# * % HP".
iExists F, P. iFrame. iIntros "!#" (E ?) "HP".
iMod ("AShft" with "[%] HP") as (x) "[H↦ Hclose]"; first done.
iModIntro. iExists (#x, 1%Qp). iFrame. iSplit.
{ iDestruct "Hclose" as "[Hclose _]". iApply "Hclose". }
......
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