Adapt to https://github.com/rocq-prover/rocq/pull/21611

[proux01]

Adapt to rocq-prover/rocq#21611

This is backward compatible.

[Janno]

This is a bit odd. m:{ x & .. } was defined to be similar to { x & .. }. Are both notations going to be illegal in the future? I don't see changes to Specif.v in the rocq PR.

[proux01]

{ x & z } is fine, the issue comes with x .. y & _ with x, y binder since now & _ will be parsed as another binder so the notation simply becomes impossible to parse, like if you were to define some x .. y ( z : w ). notation with x, y binder, any concrete ( _ : _ ) would be parsed a a binder in the x .. y sequence.

[Janno]

I see. I missed the difference in recursiveness. I will try to push a change that makes these notations non-recursive. They should actually be used somewhere so changing to | instead of & is not the ideal solutions.

[proux01]

If you want to keep the recursivity, maybe something like x , .. , y & z would work (at least that wouldn't require changing the use with a single binder)

[proux01]

Indeed, here is a solution that keeps the uses with a single binder (without change) while still allowing some kind of recursive version

[proux01]

@Janno would the current solution work?

[Janno]

Sorry, I lost track of this. I just tested your changes and I they work for me. Thanks!

[proux01]

Thanks