From 0c437537d5931f2043073eeabda1c5111210bc8c Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 13 Nov 2023 12:15:03 +0100
Subject: [PATCH] Remove superfluous unfolds

---
 theories/typing/own.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/typing/own.v b/theories/typing/own.v
index 0e85a682..4c5e65a2 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. 
-    unfold heap_pointsto_vec at 1. iSplitL; iFrame "∗#"; auto.
+    iFrame "∗#"; auto.
   Qed.
 
   Lemma read_own_move E L ty n :
@@ -245,7 +245,7 @@ Section typing.
     iDestruct "Hown" as "[H↦ $]". iDestruct "H↦" as (vl) "[>H↦ Hown]".
     iDestruct (ty_size_eq with "Hown") as "#>%".
     iExists l, vl, _. iSplitR; first done. 
-    unfold heap_pointsto_vec. iSplitL "H↦"; iFrame "∗#"; auto.
+    iFrame; auto.
     by iIntros "!> $".
   Qed.
 
-- 
GitLab