From 55de8385725053679fe2a26bfd52219d08ef8afd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 May 2017 10:52:32 +0200
Subject: [PATCH] fix compile
---
theories/typing/lib/spawn.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index a7f02d57..c0990ebe 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -106,7 +106,7 @@ Section spawn.
iIntros "?". by iFrame. }
iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
(* FIXME this is horrible. *)
- refine (let Hcall := type_call' _ [] [] f' [] [env:expr]
+ refine (let Hcall := type_call' _ [] [] [] f' [env:expr]
(λ _:(), FP_wf ∅ [# fty] retty) in _).
specialize (Hcall (rec: "_k" ["r"] := finish [ #c; "r"])%V ()).
erewrite of_val_unlock in Hcall; last done.
--
GitLab