From d853057497c7284c6c9c21a40c4167bfa1f7c0ee Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 17 Feb 2016 13:16:38 +0100
Subject: [PATCH] use the new bigOp singleton stuff

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

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 665c51d4d..7a0a9bb2d 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -144,8 +144,8 @@ Section proof.
       rewrite -(exist_intro (const P)) /=. rewrite -[saved_prop_own _ _](left_id True%I (★)%I).
       apply sep_mono.
       + rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-        admit. (* TODO: singleton set bigop. *)
-      + admit. (* TODO: singleton set bigop. *)
+        by rewrite big_sepS_singleton.
+      + by rewrite big_sepS_singleton.
     - rewrite (sts_alloc (barrier_inv l P) ⊤ N); last by eauto. rewrite !pvs_frame_r !pvs_frame_l. 
       rewrite pvs_trans'. apply pvs_strip_pvs. rewrite sep_exist_r sep_exist_l. apply exist_elim=>γ.
       (* TODO: The record notation is rather annoying here *)
-- 
GitLab