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

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

diff --git a/theories/hocap/concurrent_runners.v b/theories/hocap/concurrent_runners.v
index 476708f3..cfe0063c 100644
--- a/theories/hocap/concurrent_runners.v
+++ b/theories/hocap/concurrent_runners.v
@@ -228,7 +228,7 @@ Section contents.
     iMod (inv_alloc (N.@"task") _ (task_inv γ γ' status res (Q a))%I with "[-HP HΦ Htask Hinit]") as "#Hinv".
     { iNext. iLeft. iFrame. }
     wp_pures. iModIntro. iApply "HΦ".
-    unfold isTask, task. iFrame "#∗". eauto.
+    iFrame "#∗". eauto.
   Qed.
 
   Lemma task_Join_spec γb γ γ' (r t a : val) P Q :
-- 
GitLab