From 099b688c1ebb04e22462e8b3d0ab78d77a3e6fc2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Nov 2022 16:42:07 +0100
Subject: [PATCH] Use `binder` in notations for big ops.

---
 iris/bi/notation.v | 34 ++++++++++++++++++----------------
 1 file changed, 18 insertions(+), 16 deletions(-)

diff --git a/iris/bi/notation.v b/iris/bi/notation.v
index 4ca6fddcb..d7f411027 100644
--- a/iris/bi/notation.v
+++ b/iris/bi/notation.v
@@ -124,66 +124,68 @@ Reserved Notation "P ={ E }▷=∗^ n Q"
 
 (** * Big Ops *)
 Reserved Notation "'[∗' 'list]' k ↦ x ∈ l , P"
-  (at level 200, l at level 10, k, x at level 1, right associativity,
+  (at level 200, l at level 10, k binder, x binder, 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,
+  (at level 200, l at level 10, x binder, right associativity,
    format "[∗  list]  x  ∈  l ,  P").
 
 Reserved Notation "'[∗' 'list]' k ↦ x1 ; x2 ∈ l1 ; l2 , P"
-  (at level 200, l1, l2 at level 10, k, x1, x2 at level 1, right associativity,
+  (at level 200, l1, l2 at level 10, k binder, x1 binder, x2 binder,
+   right associativity,
    format "[∗  list]  k ↦ x1 ; x2  ∈  l1 ; l2 ,  P").
 Reserved Notation "'[∗' 'list]' x1 ; x2 ∈ l1 ; l2 , P"
-  (at level 200, l1, l2 at level 10, x1, x2 at level 1, right associativity,
+  (at level 200, l1, l2 at level 10, x1 binder, x2 binder, right associativity,
    format "[∗  list]  x1 ; x2  ∈  l1 ; l2 ,  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,
+  (at level 200, l at level 10, k binder, x binder, 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,
+  (at level 200, l at level 10, x binder, 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,
+  (at level 200, l at level 10, k binder, x binder, 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,
+  (at level 200, l at level 10, x binder, 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,
+  (at level 200, m at level 10, k binder, x binder, 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,
+  (at level 200, m at level 10, x binder, right associativity,
    format "[∗  map]  x  ∈  m ,  P").
 
 Reserved Notation "'[∗' 'map]' k ↦ x1 ; x2 ∈ m1 ; m2 , P"
-  (at level 200, m1, m2 at level 10, k, x1, x2 at level 1, right associativity,
+  (at level 200, m1, m2 at level 10,
+   k binder, x1 binder, x2 binder, right associativity,
    format "[∗  map]  k ↦ x1 ; x2  ∈  m1 ; m2 ,  P").
 Reserved Notation "'[∗' 'map]' x1 ; x2 ∈ m1 ; m2 , P"
-  (at level 200, m1, m2 at level 10, x1, x2 at level 1, right associativity,
+  (at level 200, m1, m2 at level 10, x1 binder, x2 binder, right associativity,
    format "[∗  map]  x1 ; x2  ∈  m1 ; m2 ,  P").
 
 Reserved Notation "'[∧' 'map]' k ↦ x ∈ m , P"
-  (at level 200, m at level 10, k, x at level 1, right associativity,
+  (at level 200, m at level 10, k binder, x binder, 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,
+  (at level 200, m at level 10, x binder, 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,
+  (at level 200, X at level 10, x binder, 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,
+  (at level 200, X at level 10, x binder, right associativity,
    format "[∗  mset]  x  ∈  X ,  P").
 
 (** Define the scope *)
-- 
GitLab