From e2c493dd2385aa4a444959b6a5fc08b566642cc8 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 9 Nov 2016 15:41:09 +0100
Subject: [PATCH] avoid clash of notations between disjunction and parallel
 composition

---
 heap_lang/lib/par.v          | 4 ++--
 tests/barrier_client.v       | 4 ++--
 tests/joining_existentials.v | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/heap_lang/lib/par.v b/heap_lang/lib/par.v
index 1e7904dce..ad5f70a67 100644
--- a/heap_lang/lib/par.v
+++ b/heap_lang/lib/par.v
@@ -10,7 +10,7 @@ Definition par : val :=
     let: "v2" := Snd "fs" #() in
     let: "v1" := join "handle" in
     ("v1", "v2").
-Notation "e1 || e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
+Notation "e1 ||| e2" := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E : expr_scope.
 Global Opaque par.
 
 Section proof.
@@ -39,7 +39,7 @@ Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ)
     (e1 e2 : expr) `{!Closed [] e1, Closed [] e2} (Φ : val → iProp Σ) :
   (heap_ctx ∗ WP e1 {{ Ψ1 }} ∗ WP e2 {{ Ψ2 }} ∗
    ∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V)
-  ⊢ WP e1 || e2 {{ Φ }}.
+  ⊢ WP e1 ||| e2 {{ Φ }}.
 Proof.
   iIntros "(#Hh&H1&H2&H)". iApply (par_spec Ψ1 Ψ2 with "[- $Hh $H]"); try wp_done.
   iSplitL "H1"; by wp_let.
diff --git a/tests/barrier_client.v b/tests/barrier_client.v
index 0fe8dea52..408bb502c 100644
--- a/tests/barrier_client.v
+++ b/tests/barrier_client.v
@@ -9,8 +9,8 @@ Definition worker (n : Z) : val :=
 Definition client : expr :=
   let: "y" := ref #0 in
   let: "b" := newbarrier #() in
-  ("y" <- (λ: "z", "z" + #42) ;; signal "b") ||
-    (worker 12 "b" "y" || worker 17 "b" "y").
+  ("y" <- (λ: "z", "z" + #42) ;; signal "b") |||
+    (worker 12 "b" "y" ||| worker 17 "b" "y").
 Global Opaque worker client.
 
 Section client.
diff --git a/tests/joining_existentials.v b/tests/joining_existentials.v
index 581cf8a16..0652b491f 100644
--- a/tests/joining_existentials.v
+++ b/tests/joining_existentials.v
@@ -20,7 +20,7 @@ Proof. apply subG_inG. Qed.
 
 Definition client eM eW1 eW2 : expr :=
   let: "b" := newbarrier #() in
-  (eM ;; signal "b") || ((wait "b" ;; eW1) || (wait "b" ;; eW2)).
+  (eM ;; signal "b") ||| ((wait "b" ;; eW1) ||| (wait "b" ;; eW2)).
 Global Opaque client.
 
 Section proof.
-- 
GitLab