From 02cd490ec07dae6d7930c95c91e2ba11d84ab056 Mon Sep 17 00:00:00 2001 From: rudynicolop Date: Sat, 9 Nov 2024 15:11:59 +0100 Subject: [PATCH] fixed typo --- exercises/structured_conc.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/exercises/structured_conc.v b/exercises/structured_conc.v index b8ecd63..64b4e91 100644 --- a/exercises/structured_conc.v +++ b/exercises/structured_conc.v @@ -336,7 +336,7 @@ Context `{!heapGS Σ, !tokenG Σ}. (** It is actually quite straightforward to prove the [par] specification - as most of the heavy lifting is done by [spawn_spec] and [par_spec]. + as most of the heavy lifting is done by [spawn_spec] and [join_spec]. *) Lemma par_spec (P1 P2 : iProp Σ) (e1 e2 : expr) (Q1 Q2 : val → iProp Σ) : {{{ P1 }}} e1 {{{ v, RET v; Q1 v }}} -∗