Merge branch 'ralf/propset-notation' into 'master'

make levels consistent between propset notation and singleton notation

See merge request !578

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.