From 56d13a1db2c8151e149eccbeb59431b335c1b2dd Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 24 Apr 2017 15:32:28 +0200
Subject: [PATCH] more missing Send/Sync bounds

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

diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 8f2715c7..aa8eb563 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -56,6 +56,9 @@ Section join_handle.
   Qed.
   Global Instance join_handle_ne : NonExpansive join_handle.
   Proof. apply type_contractive_ne, _. Qed.
+
+  (* TODO: Looks like in Rust, we have T: Send -> JoinHandle<T>: Send and
+     T:Sync -> JoinHandle<T>: Sync. *)
 End join_handle.
 
 Section spawn.
-- 
GitLab