From 360cb44f0166fe06126d62d1f97045102eef2116 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 May 2017 14:30:38 +0200
Subject: [PATCH] fix FIXME
---
theories/typing/lib/spawn.v | 3 +--
1 file changed, 1 insertion(+), 2 deletions(-)
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 9157cf7e..6e66ef5c 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 :
--
GitLab