From 2f8323155a40cfd1da9afb2abe27ef1bba201268 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 May 2017 14:27:48 +0200
Subject: [PATCH] fix build

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

diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 65d7d3c2..9157cf7e 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -99,18 +99,18 @@ Section spawn.
     iApply (type_let _ _ _ _ ([f' ◁ _; env ◁ _])
                      (λ j, [j ◁ join_handle retty])); try solve_typing; [|].
     { (* The core of the proof: showing that spawn is safe. *)
-      iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]".
+      iIntros (tid) "#LFT #HE $ $ [Hf' [Henv _]]". rewrite !tctx_hasty_val [fn _]lock.
       iApply (spawn_spec _ (join_inv tid retty) with "[-]");
                               first solve_to_val; last first; last simpl_subst.
       { iIntros "!> *". rewrite tctx_interp_singleton tctx_hasty_val.
         iIntros "?". by iFrame. }
-      iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let.
+      iIntros (c) "Hfin". iMod na_alloc as (tid') "Htl". wp_let. wp_let. unlock.
       iApply (type_call_iris _ [] tt 1%Qp with "LFT HE Htl [] [Hf'] [Henv]"). 4: iExact "Hf'". (* FIXME: Removing the [ ] around Hf' in the spec pattern diverges. *)
       - solve_typing.
       - solve_to_val.
       - iApply lft_tok_static.
       - iSplitL; last done. (* FIXME: iSplit should work, the RHS is persistent. *)
-        rewrite !tctx_hasty_val. iApply @send_change_tid. done.
+        rewrite tctx_hasty_val. iApply @send_change_tid. done.
       - iIntros (r) "Htl _ Hret".
         wp_rec. iApply (finish_spec with "[$Hfin Hret]"); last auto.
         by iApply @send_change_tid. }
-- 
GitLab