fix build

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. }