From 6cd508b1885781260b73ac6eb189ba5c8976907f Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 23 Feb 2016 20:06:09 +0100
Subject: [PATCH] now that we have sealing, ecancel works even in barrier.v

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

diff --git a/barrier/barrier.v b/barrier/barrier.v
index 661c155b3..b9504e560 100644
--- a/barrier/barrier.v
+++ b/barrier/barrier.v
@@ -284,7 +284,8 @@ Section proof.
       rewrite /recv /send. rewrite -(exist_intro γ) -(exist_intro P).
       rewrite -(exist_intro P) -(exist_intro i) -(exist_intro γ).
       (* This is even more annoying than usually, since rewrite sometimes unfolds stuff... *)
-      rewrite [barrier_ctx _ _ _]lock !assoc [(_ ★locked _)%I]comm !assoc -lock.
+      rewrite [barrier_ctx _ _ _]lock !assoc
+              [(_ ★ locked (barrier_ctx _ _ _))%I]comm !assoc -lock.
       rewrite -always_sep_dup.
       (* TODO: This is cancelling below a pvs. *)
       rewrite [barrier_ctx _ _ _]lock always_and_sep_l -!assoc assoc -lock.
@@ -418,8 +419,8 @@ Section proof.
       rewrite -(waiting_split _ _ _ Q R1 R2); [|done..].
       rewrite {1}[saved_prop_own i1 _]always_sep_dup.
       rewrite {1}[saved_prop_own i2 _]always_sep_dup.
-      cancel [saved_prop_own i1 R1; saved_prop_own i2 R2; l ↦ '0;
-              waiting P I; Q -★ R1 ★ R2; saved_prop_own i Q]%I.
+      ecancel [l ↦ _; saved_prop_own i1 _; saved_prop_own i2 _; waiting _ _;
+               _ -★ _; saved_prop_own i _]%I. 
       apply wand_intro_l. rewrite !assoc. eapply pvs_wand_r. rewrite /recv.
       rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
       rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
@@ -446,8 +447,8 @@ Section proof.
       rewrite -(ress_split _ _ _ Q R1 R2); [|done..].
       rewrite {1}[saved_prop_own i1 _]always_sep_dup.
       rewrite {1}[saved_prop_own i2 _]always_sep_dup.
-      cancel [saved_prop_own i1 R1; saved_prop_own i2 R2; l ↦ '1;
-              Q -★ R1 ★ R2; saved_prop_own i Q; ress I]%I.
+      ecancel [l ↦ _; saved_prop_own i1 _; saved_prop_own i2 _; ress _;
+               _ -★ _; saved_prop_own i _]%I. 
       apply wand_intro_l. rewrite !assoc. eapply pvs_wand_r. rewrite /recv.
       rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R1) -(exist_intro i1).
       rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro R2) -(exist_intro i2).
-- 
GitLab