From d25bd6a686b032e82f2d9ac0c04f47109d4be556 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 24 Oct 2024 10:08:27 +0200
Subject: [PATCH] make levels consistent between propset notation and singleton
 notation

---
 stdpp/propset.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/stdpp/propset.v b/stdpp/propset.v
index 7a220edc..c1f62c2e 100644
--- a/stdpp/propset.v
+++ b/stdpp/propset.v
@@ -6,13 +6,14 @@ Record propset (A : Type) : Type := PropSet { propset_car : A → Prop }.
 Add Printing Constructor propset.
 Global Arguments PropSet {_} _ : assert.
 Global Arguments propset_car {_} _ _ : assert.
-(** Here we are using the notation "at level 200 as pattern" because we want to
+(** Here we are using the notation "as pattern" because we want to
     be compatible with all the rules that start with [ {[ TERM ] such as
     records, singletons, and map singletons. See
     https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#binders-bound-in-the-notation-and-parsed-as-terms
-    and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003 *)
+    and https://gitlab.mpi-sws.org/iris/stdpp/-/merge_requests/533#note_98003.
+    We don't set a level to be consistent with the notation for singleton sets. *)
 Notation "{[ x | P ]}" := (PropSet (λ x, P))
-  (at level 1, x at level 200 as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
+  (at level 1, x as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
 
 Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.
 
-- 
GitLab