Skip to content
Snippets Groups Projects
Commit 0c437537 authored by Ike Mulder's avatar Ike Mulder
Browse files

Remove superfluous unfolds

parent ebd06e13
No related branches found
No related tags found
1 merge request!35Fix broken proofs for improved iFrame ∃
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
theories/typing/own.v
+ 2
− 2
View file @ 0c437537
...@@ -234,7 +234,7 @@ Section typing. ...@@ -234,7 +234,7 @@ Section typing.
iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done. iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]". iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iSplitR; first done. iExists l, _, _. iSplitR; first done.
unfold heap_pointsto_vec at 1. iSplitL; iFrame "∗#"; auto. iFrame "∗#"; auto.
Qed. Qed.
Lemma read_own_move E L ty n : Lemma read_own_move E L ty n :
...@@ -245,7 +245,7 @@ Section typing. ...@@ -245,7 +245,7 @@ Section typing.
iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]". iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
iDestruct (ty_size_eq with "Hown") as "#>%". iDestruct (ty_size_eq with "Hown") as "#>%".
iExists l, vl, _. iSplitR; first done. iExists l, vl, _. iSplitR; first done.
unfold heap_pointsto_vec. iSplitL "H↦"; iFrame "∗#"; auto. iFrame; auto.
by iIntros "!> $". by iIntros "!> $".
Qed. Qed.
......
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