From 79c74d54ccfcde24b3cb49d9424ae40f22ea64ab Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org>
Date: Tue, 25 Oct 2016 15:52:37 +0200
Subject: [PATCH] Fix comment about functions not being Send.
---
type.v | 9 ++++-----
1 file changed, 4 insertions(+), 5 deletions(-)
diff --git a/type.v b/type.v
index f77bea9f..cc91cccc 100644
--- a/type.v
+++ b/type.v
@@ -489,11 +489,6 @@ Section types.
{| st_size := n; st_own tid vl := (length vl = n)%I |}.
Next Obligation. done. Qed.
- (* TODO : For now, functions and closures are not Sync nor
- Send. This means they cannot be called in another thread than the
- one that created it.
- We will need Send and Sync closures when dealing with
- multithreading (spawn needs a Send closure). *)
Program Definition cont {n : nat} (ρ : vec val n → @perm Σ) :=
{| ty_size := 1; ty_dup := false;
ty_own tid vl := (∃ f, vl = [f] ★
@@ -508,6 +503,10 @@ Section types.
Next Obligation. intros. by iIntros "_ _". Qed.
Next Obligation. done. Qed.
+ (* TODO : For now, functions are not Send. This means they cannot be
+ called in another thread than the one that created it. We will
+ need Send functions when dealing with multithreading ([fork]
+ needs a Send closure). *)
Program Definition fn {A n} (ρ : A -> vec val n → @perm Σ) : type :=
{| st_size := 1;
st_own tid vl := (∃ f, vl = [f] ★ ∀ x vl,
--
GitLab