Allow pattern and type annotations in propset notation

Ok this doesn't work, I didn't realize that. Coq already can't make a difference with a singleton. This is annoying, I'll try to fix it

added 1 commit

fb5c6950 - Add a pattern variant of the propset notation

Compare with previous version

changed the description

added 1 commit

1f32c75a - Add a pattern variant of the propset notation

Compare with previous version

changed title from Allow propset notation to use full binders to Add new propset notations

changed the description

You might be running into https://github.com/coq/coq/issues/16042

Might be worth looking at how we have done this for big ops in Iris, iris!867 (merged)

added 1 commit

e87b3a26 - Allow patterns and type annotations in propset notation

Compare with previous version

I found the correct dark corner of the Coq manual to do this: https://coq.inria.fr/refman/user-extensions/syntax-extensions.html#binders-bound-in-the-notation-and-parsed-as-terms. With this one can write {[ (a,b) : A * B | a = b]} without any grammar ambiguity. Basically the rule still technically starts as {[ TERM, but then when the full grammar rule for propset is reduced, Coq will check that the bit before the | is actually a pattern, and otherwise fail to reduce. It allows a pattern with a type annotation because it's in a binder position in the target of the notation

Great. Would be good to have some tests to let CI check that it keeps on working.

What ever you do, please leave comments in the code that explain anything unusual that's going on, and links to wherever one can learn more about the involved tricks if applicable (like that link to the Coq reference).

Also, the MR description seems out-of-sync with the MR contents.