Allow pattern and type annotations in propset notation

This allows to use patterns and type annotations in the propset notation, Like {[ (x,y) | ... ]} or {[ x : T | ...]} or even {[ (x, y) : A * B | ...]}.

However, for both the old and new notation, this notation immediately break if someone adds a binary infix | notation downstream, In which case this will be parsed as a singleton of whatever the result of the | operation is. This was already the case before, so anyone that did that already broke the original propset notation

CHANGELOG.md

@@ -27,8 +27,8 @@ Coq 8.19 is newly supported by this version of std++.
   These tactics support both named hypotheses (`inv H`) and using a number
   to refer to a hypothesis on the goal (`inv 1`).
 - Add `prod_swap : A * B → B * A` and some basic theory about it.
-- Allow patterns and type annotations in propset notation, e.g.
-  `{[ (x, y) : nat * nat | x = y ]}`
+- Allow patterns and type annotations in `propset` notation, e.g.,
+  `{[ (x, y) : nat * nat | x = y ]}`. (by Thibaut Pérami)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).