Allow abbreviations when global references are expected, including for 8.12's auto using 0

[Blaisorblade]

To minimize surprise for the user, I think that

abbreviations should be resolved to the underlying global reference instead of being rejected where a global reference is expected.
(as @Zimmi48 agreed in #12512 (comment)).

I'd expect that for nullary abbreviations — Notation foo := bar. — and hope that allows using auto using 0 rather than auto using O.

In fact, I'd even like the same treatment for actual nullary notations, and not just abbreviations. My (naive?) plan was to parse global references using the term parser and post-process the result, to translate strings into the corresponding notations (and underlying references) and filter out terms that aren't references.

EDIT: part of my argument is that (1) 0 and O are usually interchangeable (2) explaining that they aren't via current Coq parse errors is not a great UX.

[Blaisorblade]

Tagging for 8.12 because this reduces the regressions from #12512.

[Blaisorblade]

And tagging @herbelin, I guess, since this is about parsing.

[Zimmi48]

Sorry, but this is out of scope for 8.12.

[Blaisorblade]

No worries, it's your job to say no — and #12512 seems not scheduled for 8.12.

[herbelin]

And tagging @herbelin, I guess, since this is about parsing.

Hi, just commenting about the 0: I agree that 0 and O are interchangeable. On the other side, the generality of supporting 0 in auto using is not clear to me. Would the rule to accept any numeral that is interpreted as a global reference? In this case 0, 0%Z or 1%positive would be allowed, but 1, 1%Z or 0%R would be rejected (since not bound to an expression reducing to a global reference)?

[Zimmi48]

As discussed privately with @herbelin yesterday, 0 is not an abbreviation, so it would require special treatment of numerals (as hinted by @herbelin above). However, I'm fully supportive of accepting smart_global, which would include things like abbreviations and notations represented by a string, if ever the support for terms in the using clause is removed (this is really tied to #12512---which is definitely not scheduled for 8.12 😆).