diff --git a/theories/lang/spawn.v b/theories/lang/spawn.v index 93612750b69f26dfd8484f4ce20b3d8a035006a1..17d92893aeb511c7a2d66c16412623f3d355e8c6 100644 --- a/theories/lang/spawn.v +++ b/theories/lang/spawn.v @@ -20,8 +20,8 @@ Definition finish : val := Definition join : val := rec: "join" ["c"] := if: !ˢᶜ"c" then - let: "v" := !("c" +ₗ #1) in (* The thread finished, we can non-atomically load the data. *) + let: "v" := !("c" +ₗ #1) in Free #2 "c";; "v" else