From 123a7c050d9e112e33aa8a612d751f92359ffef5 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 27 Sep 2016 10:01:02 +0200
Subject: [PATCH] Big ops over gmap without binder for the key.

---
 algebra/cmra_big_op.v  | 3 +++
 algebra/upred_big_op.v | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/algebra/cmra_big_op.v b/algebra/cmra_big_op.v
index 58d580778..b9f814a95 100644
--- a/algebra/cmra_big_op.v
+++ b/algebra/cmra_big_op.v
@@ -44,6 +44,9 @@ Typeclasses Opaque big_opM.
 Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM m (λ k x, P))
   (at level 200, m at level 10, k, x at level 1, right associativity,
    format "[⋅  map ]  k ↦ x  ∈  m ,  P") : C_scope.
+Notation "'[⋅' 'map' ] x ∈ m , P" := (big_opM m (λ _ x, P))
+  (at level 200, m at level 10, x at level 1, right associativity,
+   format "[⋅  map ]  x  ∈  m ,  P") : C_scope.
 
 Definition big_opS {M : ucmraT} `{Countable A}
   (X : gset A) (f : A → M) : M := [⋅] (f <$> elements X).
diff --git a/algebra/upred_big_op.v b/algebra/upred_big_op.v
index c9ae5148c..64aed4cf4 100644
--- a/algebra/upred_big_op.v
+++ b/algebra/upred_big_op.v
@@ -47,6 +47,9 @@ Typeclasses Opaque uPred_big_sepM.
 Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
   (at level 200, m at level 10, k, x at level 1, right associativity,
    format "[★  map ]  k ↦ x  ∈  m ,  P") : uPred_scope.
+Notation "'[★' 'map' ] x ∈ m , P" := (uPred_big_sepM m (λ _ x, P))
+  (at level 200, m at level 10, x at level 1, right associativity,
+   format "[★  map ]  x  ∈  m ,  P") : uPred_scope.
 
 Definition uPred_big_sepS {M} `{Countable A}
   (X : gset A) (Φ : A → uPred M) : uPred M := [★] (Φ <$> elements X).
-- 
GitLab