Skip to content
Snippets Groups Projects
Commit c788b94e authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Thou shalt not use generated names.

parent 3e2074fd
No related branches found
No related tags found
No related merge requests found
Pipeline #119813 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/lifetime/model/accessors.v
+ 2
− 2
View file @ c788b94e
...@@ -167,7 +167,7 @@ Proof. ...@@ -167,7 +167,7 @@ Proof.
iMod ("Hclose'" with "[-Hbor Hclose]") as "_". iMod ("Hclose'" with "[-Hbor Hclose]") as "_".
{ iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''". { iExists _, _. iFrame. rewrite big_sepS_later. iApply "Hclose''".
iLeft. iFrame "%". iExists _, _. iFrame. } iLeft. iFrame "%". iExists _, _. iFrame. }
iExists κ''. iFrame "#". iIntros "!>* HvsQ HQ". clear -HE. iExists κ''. iFrame "#". iIntros "!> %Q HvsQ HQ". clear -HE.
iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'". iInv mgmtN as (A I) "(>HA & >HI & Hinv)" "Hclose'".
iDestruct (own_bor_auth with "HI Hbor") as %Hκ'. iDestruct (own_bor_auth with "HI Hbor") as %Hκ'.
rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom // rewrite big_sepS_later big_sepS_elem_of_acc ?elem_of_dom //
...@@ -235,7 +235,7 @@ Proof. ...@@ -235,7 +235,7 @@ Proof.
as %[EQB%to_borUR_included _]%auth_both_valid_discrete. as %[EQB%to_borUR_included _]%auth_both_valid_discrete.
iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)". iMod (slice_delete_full _ _ true with "Hs Hbox") as (Pb') "(HP' & EQ & Hbox)".
solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$". solve_ndisj. by rewrite lookup_fmap EQB. iDestruct ("HPP'" with "HP'") as "$".
iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose * HvsQ HQ". iApply fupd_mask_intro; [solve_ndisj|]. iIntros "Hclose %Q HvsQ HQ".
iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs". iMod "Hclose" as "_". iDestruct (add_vs with "EQ Hvs [HvsQ]") as "Hvs".
{ iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). } { iNext. iIntros "HQ H†". iApply "HPP'". iApply ("HvsQ" with "HQ H†"). }
iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)". iMod (slice_insert_full _ _ true with "HQ Hbox") as (j) "(% & #Hs' & Hbox)".
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment