diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v index 9157cf7edfa933751e08a0b6b15b4a84831fcbd3..6e66ef5cf70d6d2efca11b49435faa85a2bc1c74 100644 --- a/theories/typing/lib/spawn.v +++ b/theories/typing/lib/spawn.v @@ -62,8 +62,7 @@ Section join_handle. Proof. iIntros (??? vl) "Hvl". destruct vl as [|[[|vl|]|] [|]]; try done. simpl. iApply (join_handle_impl with "[] Hvl"). iIntros "!# * Hv". - unfold join_inv. iApply own_send. (* FIXME: Why does "iApply send_change_tid" not work? *) - done. + unfold join_inv. iApply @send_change_tid. done. Qed. Global Instance join_handle_sync ty :