Incompatible prefix warning

I had to silence the following warning to get CI to pass on Coq 8.20:

File "./stdpp/propset.v", line 14, characters 0-128:
Warning: Notations "{[ _ ]}" defined at level 1 with arguments constr
and "{[ _ | _ ]}" defined at level 1 with arguments constr  as pattern
at level 200 have incompatible prefixes. One of them will likely not work.
[notation-incompatible-prefix,parsing,default]

That sounds like something we should fix?