Adapt to https://github.com/coq/coq/pull/18224

@jung no hurry (the upstream PR https://github.com/coq/coq/pull/18224 is targeting Coq 8.20) but would be nice to merge this one at some point

I'm afraid I have no idea what this change will do for our users. Coq notation levels are black box magic to me. Maybe @robbertkrebbers has an idea.

Could you explain why the Coq PR requires the level of the projection notations to be changed?

These notations were at level 2 to be compatible with ssreflect., i.e., to make sure one can import both ssreflect and std++ and not get conflicts, see 5c069266.

I see the Coq PR also changes the ssreflect notation, so that is good.

However, std++ attempts to be compatible with the last two versions of Coq. After we merge this, Iris won't be compatible with the ssr in a released Coq version, so that will be a problem. Any idea what to do about that?

However, std++ attempts to be compatible with the last two versions of Coq. After we merge this, Iris won't be compatible with the ssr in a released Coq version, so that will be a problem. Any idea what to do about that?

The lack of support for conditional compilation strikes again... ideally we could just do

#[cfg(coq-version >= (8, 20))]
Notation ...
#[cfg(coq-version < (8, 20))]
Notation ...

The goal is to enable at some point in the future to remove the recovery mechanism of camlp5/coqpp so as to be able to actually implement no-associativity and easier mixing of left and right associativiy for instance. Once this done, the postfix notations like _.1 should be at level 1 if we want to still be able to write _.1%scope and not (_.1)%scope.

I don't have a solution right now for backward compatibility but have some ideas (something like at existing level or <n>), so let me close this and come back later with a solution once this is implemented in Coq (so maybe next year, two Coq versions later).

closed

ssreflect is in Coq now. Why does std++ have to set a level at all, can't it import the ssreflect notation?

Alternatively, putting a Reserved Notation into some Coq file imported by both std++ and ssreflect would work (but also incurs a delay, we can only remove the level in std++ once we require a Coq that has the Reserved Notation).