From ba676fcb39478d2af312285125f55d586dd005b1 Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Wed, 6 Mar 2024 10:21:18 +0100
Subject: [PATCH] Fix proof after iris/iris!1035.

---
 theories/typing/own.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/own.v b/theories/typing/own.v
index 4c5e65a2..fe897cbf 100644
--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -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 :
-- 
GitLab