diff --git a/stdpp/propset.v b/stdpp/propset.v
index 1ed3af52c216d25065133279d39c7b2481216f68..5c829eb6c015e9a784929b89ecd41443d729b763 100644
--- a/stdpp/propset.v
+++ b/stdpp/propset.v
@@ -7,7 +7,7 @@ Add Printing Constructor propset.
 Global Arguments PropSet {_} _ : assert.
 Global Arguments propset_car {_} _ _ : assert.
 Notation "{[ x | P ]}" := (PropSet (λ x, P))
-  (at level 1, format "{[  x  |  P  ]}") : stdpp_scope.
+  (at level 1, x at level 200 as pattern, format "{[  x  |  P  ]}") : stdpp_scope.
 
 Global Instance propset_elem_of {A} : ElemOf A (propset A) := λ x X, propset_car X x.