From 49b0451545856d67b32c3a8ee5fb940157988f2a Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Jan 2019 22:11:09 +0100
Subject: [PATCH] avoid non-value notation in val_scope

---
 theories/heap_lang/lib/coin_flip.v | 2 +-
 theories/heap_lang/lib/par.v       | 4 +---
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/heap_lang/lib/coin_flip.v b/theories/heap_lang/lib/coin_flip.v
index 57b085436..7e3569b1e 100644
--- a/theories/heap_lang/lib/coin_flip.v
+++ b/theories/heap_lang/lib/coin_flip.v
@@ -1,7 +1,7 @@
 From iris.base_logic.lib Require Export invariants.
 From iris.program_logic Require Export atomic.
 From iris.proofmode Require Import tactics.
-From iris.heap_lang Require Import proofmode notation par.
+From iris.heap_lang Require Import proofmode notation.
 Set Default Proof Using "Type".
 
 (** Nondeterminism and Speculation:
diff --git a/theories/heap_lang/lib/par.v b/theories/heap_lang/lib/par.v
index 0d55d3a4b..34c6ad2e7 100644
--- a/theories/heap_lang/lib/par.v
+++ b/theories/heap_lang/lib/par.v
@@ -12,8 +12,6 @@ Definition par : val :=
     let: "v1" := join "handle" in
     ("v1", "v2").
 Notation "e1 ||| e2" := (par (λ: <>, e1)%E (λ: <>, e2)%E) : expr_scope.
-(* Not a value itself, but with *unlocked* value lambdas. *)
-Local Notation "e1 ||| e2" := (par (LamV BAnon e1%E) (LamV BAnon e2%E)) : val_scope.
 
 Section proof.
 Local Set Default Proof Using "Type*".
@@ -39,7 +37,7 @@ Qed.
 Lemma wp_par (Ψ1 Ψ2 : val → iProp Σ) (e1 e2 : expr) (Φ : val → iProp Σ) :
   WP e1 {{ Ψ1 }} -∗ WP e2 {{ Ψ2 }} -∗
   (∀ v1 v2, Ψ1 v1 ∗ Ψ2 v2 -∗ ▷ Φ (v1,v2)%V) -∗
-  WP (e1 ||| e2)%V {{ Φ }}.
+  WP par (LamV BAnon e1) (LamV BAnon e2) {{ Φ }}.
 Proof.
   iIntros "H1 H2 H".
   wp_apply (par_spec Ψ1 Ψ2 with "[H1] [H2] [H]"); [by wp_lam..|auto].
-- 
GitLab