Commit 353e2900 authored by Gaurav Parthasarathy's avatar Gaurav Parthasarathy

minor change

parent dc0db6aa
Pipeline #18263 failed with stage
...@@ -387,7 +387,8 @@ Section rdcss. ...@@ -387,7 +387,8 @@ Section rdcss.
(* FIXME: proof duplication *) (* FIXME: proof duplication *)
wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail. wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
iIntros (vs'' ->) "Hp". iModIntro. iIntros (vs'' ->) "Hp". iModIntro.
iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro. iSplitL "Done Hp". { by eauto 12 with iFrame. }
iModIntro.
iSplitL "Hln Hrest". { by eauto 12 with iFrame. } iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
wp_seq. iApply "HQ". wp_seq. iApply "HQ".
iApply state_done_extract_Q; done. iApply state_done_extract_Q; done.
......
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