From 07045934fe19cea3fbde66b9eb53eb61d63bc838 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 May 2017 10:20:13 +0200
Subject: [PATCH] *oops* did not mean to commit this yet

---
 theories/typing/lib/spawn.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index ba16d840..a7f02d57 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -105,9 +105,6 @@ Section spawn.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
       iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
-      iApply (type_call_iris _ [] [] tt with "HE [] [] [Hf']"). 5: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
-      solve_typing. solve_to_val. rewrite /llctx_interp. done. iApply lft_tok_static.
-      iFrame. done.
       (* FIXME this is horrible. *)
       refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
                 (λ _:(), FP_wf ∅ [# fty] retty) in _).
-- 
GitLab