From b33a29de33fed6f406c42b711a9be1a0f30ee85a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 26 Oct 2018 11:10:33 +0200
Subject: [PATCH] =?UTF-8?q?Notation=20`P=20=3D{E1,E2}=E2=96=B7=3D=E2=88=97?=
 =?UTF-8?q?^n=20Q`.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/bi/notation.v | 3 +++
 theories/bi/updates.v  | 2 ++
 2 files changed, 5 insertions(+)

diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index c64497696..d522114bd 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -90,6 +90,9 @@ Reserved Notation "P ={ E }▷=∗ Q"
 Reserved Notation "|={ E1 , E2 }â–·=>^ n Q"
   (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
    format "|={ E1 , E2 }â–·=>^ n  Q").
+Reserved Notation "P ={ E1 , E2 }▷=∗^ n Q"
+  (at level 99, E1, E2 at level 50, n at level 9, Q at level 200,
+   format "P  ={ E1 , E2 }▷=∗^ n  Q").
 
 (** Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 40a3437b4..f36e712e1 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -33,6 +33,8 @@ Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2, E1 }▷=> Q)%I : bi_s
 Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
 Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
 Notation "|={ E1 , E2 }▷=>^ n Q" := (Nat.iter n (λ P, |={E1,E2}▷=> P) Q)%I : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P ⊢ |={E1,E2}▷=>^n Q)%I (only parsing) : stdpp_scope.
+Notation "P ={ E1 , E2 }▷=∗^ n Q" := (P -∗ |={E1,E2}▷=>^n Q)%I : bi_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
-- 
GitLab