make levels consistent between propset notation and singleton notation

This fixes the last remaining occurrences of the "incompatible prefix" warning when building with coq.dev. {[ x ]} does not set a level for x so I guess it makes sense that we have to do the same here.

Cc @tperami @Blaisorblade

changed the description

This is great.

This fixes the last remaining occurrences of the "incompatible prefix" warning when building with coq.dev.

So, with Coq 8.20 we still get such errors? Does this rely on a recent fix in Coq dev? Do you have a link?

{[ x ]} does not set a level for x so I guess it makes sense that we have to do the same here.

An alternative is to set the level for x in {[ x ]}?

mentioned in issue #216

So, with Coq 8.20 we still get such errors? Does this rely on a recent fix in Coq dev? Do you have a link?

It relies on https://github.com/coq/coq/pull/19653. It looks like that PR may be backported to 8.20 but that has not happened yet.

An alternative is to set the level for x in {[ x ]}?

We'd have to set a level in all notations starting with {[. So this also includes {[ x ; y ; .. ; z ]} and {[ k := a ]}.

Thanks, makes sense to rely on the default level then.

If all the other same prefix notation don't specify a level, we might as well not have one here

resolved all threads

mentioned in commit 96839810

merged