Autosubst notations

[MevenBertrand]

When moving to 8.20, @kyoDralliam had to comment out a notation in the file generated by AutoSubst: there is a new warning about notations with incompatible prefixes, which this notation hits HARD. Afaict, any notation involving [ is forced by this to be set at level 1, which is quite horrible.

For now, the comment is a "hotfix", but this means we again cannot generate the Ast.v file with a simple recipe :( We really should have a better solution. @yforster do you think this should be fixed upstream in AutoSubst?

[yforster]

Probably it should be fixed either in Coq or in AutoSubst. Why is this incompatible prefix thing introduced?

What would be the fix in Autosubst? Have an option to not generate any notations? Or just use a different symbol for this notation from 8.20 on?

[MevenBertrand]

Afaiu the issue is that if you have two notations at different levels starting with the same token, the parser will have to always go for one instead of the other, which will silently be killed. This used to always exist, but there was a new added warning to let users know about it. In our case, I guess we never realised because we never use the scope Autosubst is using.

On the Autosubst side, I think we could

• remove this one particular notation, which is afaict rather unnecessary
• have an option not to generate notations at all (which would be I think a good step in the direction of saner notations anyway)

[MevenBertrand]

I just realised that uds-psl/autosubst2#8 also has beef with the exact same notation. I can't reproduce their hard error on my side, but maybe another sign we should act on this.