From 75236abc79f41fd7a44ff371c1b98d6b0d552e5c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 31 May 2018 12:07:26 +0200
Subject: [PATCH] also pre-reserve bigops notation

---
 theories/bi/big_op.v   | 54 ++++++++++++++++--------------------------
 theories/bi/notation.v | 40 +++++++++++++++++++++++++++++++
 2 files changed, 60 insertions(+), 34 deletions(-)

diff --git a/theories/bi/big_op.v b/theories/bi/big_op.v
index 277d29308..4825fd551 100644
--- a/theories/bi/big_op.v
+++ b/theories/bi/big_op.v
@@ -5,40 +5,26 @@ Set Default Proof Using "Type".
 Import interface.bi derived_laws_bi.bi.
 
 (* Notations *)
-Notation "'[∗' 'list]' k ↦ x ∈ l , P" := (big_opL bi_sep (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∗  list]  k ↦ x  ∈  l ,  P") : bi_scope.
-Notation "'[∗' 'list]' x ∈ l , P" := (big_opL bi_sep (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∗  list]  x  ∈  l ,  P") : bi_scope.
-
-Notation "'[∗]' Ps" :=
-  (big_opL bi_sep (λ _ x, x) Ps) (at level 20) : bi_scope.
-
-Notation "'[∧' 'list]' k ↦ x ∈ l , P" := (big_opL bi_and (λ k x, P) l)
-  (at level 200, l at level 10, k, x at level 1, right associativity,
-   format "[∧  list]  k ↦ x  ∈  l ,  P") : bi_scope.
-Notation "'[∧' 'list]' x ∈ l , P" := (big_opL bi_and (λ _ x, P) l)
-  (at level 200, l at level 10, x at level 1, right associativity,
-   format "[∧  list]  x  ∈  l ,  P") : bi_scope.
-
-Notation "'[∧]' Ps" :=
-  (big_opL bi_and (λ _ x, x) Ps) (at level 20) : bi_scope.
-
-Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m)
-  (at level 200, m at level 10, k, x at level 1, right associativity,
-   format "[∗  map]  k ↦ x  ∈  m ,  P") : bi_scope.
-Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m)
-  (at level 200, m at level 10, x at level 1, right associativity,
-   format "[∗  map]  x  ∈  m ,  P") : bi_scope.
-
-Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  set]  x  ∈  X ,  P") : bi_scope.
-
-Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X)
-  (at level 200, X at level 10, x at level 1, right associativity,
-   format "[∗  mset]  x  ∈  X ,  P") : bi_scope.
+Notation "'[∗' 'list]' k ↦ x ∈ l , P" :=
+  (big_opL bi_sep (λ k x, P) l) : bi_scope.
+Notation "'[∗' 'list]' x ∈ l , P" :=
+  (big_opL bi_sep (λ _ x, P) l) : bi_scope.
+
+Notation "'[∗]' Ps" := (big_opL bi_sep (λ _ x, x) Ps) : bi_scope.
+
+Notation "'[∧' 'list]' k ↦ x ∈ l , P" :=
+  (big_opL bi_and (λ k x, P) l) : bi_scope.
+Notation "'[∧' 'list]' x ∈ l , P" :=
+  (big_opL bi_and (λ _ x, P) l) : bi_scope.
+
+Notation "'[∧]' Ps" := (big_opL bi_and (λ _ x, x) Ps) : bi_scope.
+
+Notation "'[∗' 'map]' k ↦ x ∈ m , P" := (big_opM bi_sep (λ k x, P) m) : bi_scope.
+Notation "'[∗' 'map]' x ∈ m , P" := (big_opM bi_sep (λ _ x, P) m) : bi_scope.
+
+Notation "'[∗' 'set]' x ∈ X , P" := (big_opS bi_sep (λ x, P) X) : bi_scope.
+
+Notation "'[∗' 'mset]' x ∈ X , P" := (big_opMS bi_sep (λ x, P) X) : bi_scope.
 
 (** * Properties *)
 Section bi_big_op.
diff --git a/theories/bi/notation.v b/theories/bi/notation.v
index 6eedc2d83..586b5d2a1 100644
--- a/theories/bi/notation.v
+++ b/theories/bi/notation.v
@@ -1,15 +1,20 @@
 (** Just reserve the notation. *)
+
+(** Turnstiles *)
 Reserved Notation "P ⊢ Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "P '⊢@{' PROP } Q" (at level 99, Q at level 200, right associativity).
 Reserved Notation "('⊢@{' PROP } )" (at level 99).
 Reserved Notation "P ⊣⊢ Q" (at level 95, no associativity).
 Reserved Notation "P '⊣⊢@{' PROP } Q" (at level 95, no associativity).
 Reserved Notation "('⊣⊢@{' PROP } )" (at level 95).
+
+(** BI connectives *)
 Reserved Notation "'emp'".
 Reserved Notation "'⌜' φ '⌝'" (at level 1, φ at level 200, format "⌜ φ ⌝").
 Reserved Notation "P ∗ Q" (at level 80, right associativity).
 Reserved Notation "P -∗ Q" (at level 99, Q at level 200, right associativity).
 
+(** Modalities *)
 Reserved Notation "'<pers>' P" (at level 20, right associativity).
 Reserved Notation "'<pers>?' p P" (at level 20, p at level 9, P at level 20,
    right associativity, format "'<pers>?' p  P").
@@ -38,6 +43,7 @@ Reserved Notation "â–  P" (at level 20, right associativity).
 Reserved Notation "â– ? p P" (at level 20, p at level 9, P at level 20,
    right associativity, format "â– ? p  P").
 
+(** Update modalities *)
 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").
 
@@ -68,5 +74,39 @@ Reserved Notation "P ={ E }▷=∗ Q"
   (at level 99, E at level 50, Q at level 200,
    format "P  ={ E }▷=∗  Q").
 
+(** Big Ops *)
+Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k, x at level 1, right associativity,
+   format "[∗  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∗' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x at level 1, right associativity,
+   format "[∗  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∗]' Ps" (at level 20).
+
+Reserved Notation "'[∧' 'list]' k ↦ x ∈ l , P"
+  (at level 200, l at level 10, k, x at level 1, right associativity,
+   format "[∧  list]  k ↦ x  ∈  l ,  P").
+Reserved Notation "'[∧' 'list]' x ∈ l , P"
+  (at level 200, l at level 10, x at level 1, right associativity,
+   format "[∧  list]  x  ∈  l ,  P").
+
+Reserved Notation "'[∧]' Ps" (at level 20).
+
+Reserved Notation "'[∗' 'map]' k ↦ x ∈ m , P"
+  (at level 200, m at level 10, k, x at level 1, right associativity,
+   format "[∗  map]  k ↦ x  ∈  m ,  P").
+Reserved Notation "'[∗' 'map]' x ∈ m , P"
+  (at level 200, m at level 10, x at level 1, right associativity,
+   format "[∗  map]  x  ∈  m ,  P").
+
+Reserved Notation "'[∗' 'set]' x ∈ X , P"
+  (at level 200, X at level 10, x at level 1, right associativity,
+   format "[∗  set]  x  ∈  X ,  P").
+
+Reserved Notation "'[∗' 'mset]' x ∈ X , P"
+  (at level 200, X at level 10, x at level 1, right associativity,
+   format "[∗  mset]  x  ∈  X ,  P").
+
 (** Define the scope *)
 Delimit Scope bi_scope with I.
-- 
GitLab