From d822ba8a245078fb5d00ea2a9f2f4564ae4f2009 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 17:15:53 +0100
Subject: [PATCH] complete signal_spec :-)

---
 barrier/barrier.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 50569b44e..224c0e889 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -203,8 +203,9 @@ Section proof.
     (* Now we come to the core of the proof: Updating from waiting to ress. *)
     rewrite /waiting /ress sep_exist_l. apply exist_elim=>{Q} Q.
     rewrite later_wand {1}(later_intro P) !assoc wand_elim_r.
-    (* TODO: Now we need stuff about Π★{set I} *)
-  Abort.
+    rewrite -big_sepS_later -big_sepS_sepS. apply big_sepS_mono'=>i.
+    rewrite -(exist_intro (Q i)) comm. done.
+  Qed.
 
   Lemma wait_spec l P (Q : val → iProp) :
     heapN ⊥ N → (recv l P ★ (P -★ Q '())) ⊑ wp ⊤ (wait (LocV l)) Q.
-- 
GitLab