Fix #70: add pattern variant of bind notation

Use that in place of the old encoding: #70 (comment 52817)

Requires dropping support for Coq 8.7 (in a separate MR).

changed the description

Blocked on !170 (merged)

Unblocked by the merge.

Since this breaks the existing (hacky!) notation, can you add a CHANGELOG entry?

I will only merge this after the POPL deadline, since it means the reverse dependencies have to be updated.

Ping @Blaisorblade: Since @jung wants to make a release today, would you be able to add such a changelog entry?

(I wasn't actually expecting to include any of these open std++ MRs in the release. That just makes it more likely to introduce last-minute breaking changes or regressions. In general, a "rush for the release window" is almost always a bad idea.)

I agree. This surely means we need to run CI for all reverse dependencies and fix outfall (which won't be a lot, but still some).

However, since this was the reason for dropping support of Coq 8.7 it feels a bit silly not to include a fix for the current hack.

Well, let me know now what you want to do. These runs take an hour or so, we should not wait for @Blaisorblade to write a changelog entry but write it ourselves instead if we want to include this.

Ok, let's merge this, I write something.

merged

mentioned in commit 92dc4869

Let me update Iris, then you can do a CI run while I update update the CHANGELOG in parallel.

(Updating Iris is blocked on https://gitlab.mpi-sws.org/iris/stdpp/-/pipelines/31479 completing, which is waiting for https://gitlab.mpi-sws.org/iris/lambda-rust/-/jobs/79796.)

mentioned in commit 76b66f20

The new std++ is on opam now; you can update Iris.

@iris-users This is a breaking change.

CHANGELOG is here: 76b66f20

Changes to Iris are here: iris@3012972e