From f9e889858c08f6265a40c60da24be691f721b261 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 28 May 2018 13:20:37 +0200
Subject: [PATCH] reserve fancy update notation

---
 theories/bi/notation.v | 27 +++++++++++++++++++++++++++
 theories/bi/updates.v  | 40 +++++++++++-----------------------------
 2 files changed, 38 insertions(+), 29 deletions(-)

diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 40cae6817..6eedc2d83 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -41,5 +41,32 @@ Reserved Notation "â– ? p P" (at level 20, p at level 9, P at level 20,
 Reserved Notation "|==> Q" (at level 99, Q at level 200, format "|==>  Q").
 Reserved Notation "P ==∗ Q" (at level 99, Q at level 200, format "P  ==∗  Q").
 
+Reserved Notation "|={ E1 , E2 }=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }=>  Q").
+Reserved Notation "P ={ E1 , E2 }=∗ Q"
+  (at level 99, E1,E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }=∗  Q").
+
+Reserved Notation "|={ E }=> Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }=>  Q").
+Reserved Notation "P ={ E }=∗ Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }=∗  Q").
+
+Reserved Notation "|={ E1 , E2 }â–·=> Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "|={ E1 , E2 }â–·=>  Q").
+Reserved Notation "P ={ E1 , E2 }▷=∗ Q"
+  (at level 99, E1, E2 at level 50, Q at level 200,
+   format "P  ={ E1 , E2 }▷=∗  Q").
+Reserved Notation "|={ E }â–·=> Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "|={ E }â–·=>  Q").
+Reserved Notation "P ={ E }▷=∗ Q"
+  (at level 99, E at level 50, Q at level 200,
+   format "P  ={ E }▷=∗  Q").
+
 (** Define the scope *)
 Delimit Scope bi_scope with I.
diff --git a/theories/bi/updates.v b/theories/bi/updates.v
index 3a47ebd5f..a36798e9d 100644
--- a/theories/bi/updates.v
+++ b/theories/bi/updates.v
@@ -15,37 +15,19 @@ Class FUpd (PROP : Type) : Type := fupd : coPset → coPset → PROP → PROP.
 Instance: Params (@fupd) 4.
 Hint Mode FUpd ! : typeclass_instances.
 
-Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q)
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I
-  (at level 99, E1,E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }=∗  Q") : bi_scope.
-Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)
-  (at level 99, E1, E2 at level 50, Q at level 200, only parsing) : stdpp_scope.
-
-Notation "|={ E }=> Q" := (fupd E E Q)
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }=>  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }=∗  Q") : bi_scope.
-Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)
-  (at level 99, E at level 50, Q at level 200, only parsing) : stdpp_scope.
+Notation "|={ E1 , E2 }=> Q" := (fupd E1 E2 Q) : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q)%I : bi_scope.
+Notation "P ={ E1 , E2 }=∗ Q" := (P -∗ |={E1,E2}=> Q) : stdpp_scope.
+
+Notation "|={ E }=> Q" := (fupd E E Q) : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q)%I : bi_scope.
+Notation "P ={ E }=∗ Q" := (P -∗ |={E}=> Q) : stdpp_scope.
 
 (** Fancy updates that take a step. *)
-Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "|={ E1 , E2 }â–·=>  Q") : bi_scope.
-Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I
-  (at level 99, E1, E2 at level 50, Q at level 200,
-   format "P  ={ E1 , E2 }▷=∗  Q") : bi_scope.
-Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "|={ E }â–·=>  Q") : bi_scope.
-Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I
-  (at level 99, E at level 50, Q at level 200,
-   format "P  ={ E }▷=∗  Q") : bi_scope.
+Notation "|={ E1 , E2 }â–·=> Q" := (|={E1,E2}=> (â–· |={E2,E1}=> Q))%I : bi_scope.
+Notation "P ={ E1 , E2 }▷=∗ Q" := (P -∗ |={ E1 , E2 }▷=> Q)%I : bi_scope.
+Notation "|={ E }â–·=> Q" := (|={E,E}â–·=> Q)%I : bi_scope.
+Notation "P ={ E }▷=∗ Q" := (P ={E,E}▷=∗ Q)%I : bi_scope.
 
 (** Bundled versions  *)
 (* Mixins allow us to create instances easily without having to use Program *)
-- 
GitLab