Skip to content
Snippets Groups Projects
Commit 295af2d4 authored by Ralf Jung's avatar Ralf Jung
Browse files

boxes: fewer underscores

parent e4c30558
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
program_logic/boxes.v
+ 1
− 1
View file @ 295af2d4
...@@ -156,7 +156,7 @@ Proof. ...@@ -156,7 +156,7 @@ Proof.
iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]". iIntros {?} "[#Hinv H]"; iDestruct "H" as {Φ} "[#HeqP Hf]".
iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ". iInv N as {b} "(Hγ & #HγQ & HQ)"; iTimeless "Hγ".
iDestruct (big_sepM_later _ f with "Hf") as "Hf". iDestruct (big_sepM_later _ f with "Hf") as "Hf".
iDestruct (big_sepM_delete _ f _ true with "Hf") iDestruct (big_sepM_delete _ f with "Hf")
as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'". as "[[Hγ' #[HγΦ Hinv']] ?]"; first done; iTimeless "Hγ'".
iDestruct (box_own_auth_agree γ b true with "[#]") iDestruct (box_own_auth_agree γ b true with "[#]")
as "%"; subst; first by iFrame "Hγ". as "%"; subst; first by iFrame "Hγ".
......
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