Commit 4ee23161 by Robbert Krebbers

Proof mode name fixes (in preparation of Iris !83).

parent b6993ddc
Pipeline #5353 failed with stage
in 4 minutes 42 seconds
......@@ -52,7 +52,7 @@ Section na_bor.
Lemma na_bor_shorten κ κ': κ κ' - &na{κ',tid,N}P - &na{κ,tid,N}P.
Proof.
iIntros "Hκκ' H". iDestruct "H" as (i) "[??]". iExists i. iFrame.
iIntros "Hκκ' H". iDestruct "H" as (i) "[H ?]". iExists i. iFrame.
iApply (idx_bor_shorten with "Hκκ' H").
Qed.
......
......@@ -127,7 +127,7 @@ Section refcell.
iAssert ((q / 2).[κ] γ, refcell_inv tid l γ κ ty)%I with "[> -Hclose]"
as "[$ HQ]"; last first.
{ iMod ("Hclose" with "[] HQ") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
iExists _. iIntros "{$H}!%". destruct st as [[?[|[]|]]|]; simpl; lia.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iExists κ, γ. iSplitR. by iApply lft_incl_refl. by iApply bor_na. }
......
......@@ -122,7 +122,7 @@ Section rwlock.
iAssert ((q / 2).[κ] γ, rwlock_inv tid l γ κ ty)%I with "[> -Hclose]"
as "[$ HQ]"; last first.
{ iMod ("Hclose" with "[] HQ") as "[Hb $]".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(? & _ & _)".
- iIntros "!> H !>". iNext. iDestruct "H" as (γ st) "(H & _ & _)".
iExists _. iIntros "{$H}!%". destruct st as [[|[[]?]|]|]; simpl; lia.
- iMod (bor_exists with "LFT Hb") as (γ) "Hb". done.
iExists κ, γ. iSplitR. by iApply lft_incl_refl. iApply bor_share; try 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