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

Fix proof after iris/iris!1035.

parent 9003ab64
Branches
Tags
1 merge request!36Fix proof after iris/iris!1035.
......@@ -234,7 +234,7 @@ Section typing.
iIntros ([[|l|]|] tid F qmax qL ?) "_ _ $ $ Hown"; try done.
iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ #Hown]".
iExists l, _, _. iSplitR; first done.
iFrame "∗#"; auto.
iFrame "∗#". by iIntros "!> $".
Qed.
Lemma read_own_move E L ty n :
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment