Abbreviations don't add printing rule when still qualified

[SkySkimmer]

Fix #20668

Overlays (to be merged before the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/20816 stdlib#208
• Adapt to https://github.com/rocq-prover/rocq/pull/20816 mit-plv/rewriter#177
• Adapt to https://github.com/rocq-prover/rocq/pull/20816 mit-plv/fiat-crypto#2155

Overlay (to be merged in sync with the current PR)

• Adapt to https://github.com/rocq-prover/rocq/pull/20816 LPCIC/coq-elpi#883

[proux01]

@JasonGross apparently, fiat-crypto was relying on the bug in its output test, could you please prepare an overlay
I'm doing the stdlib one

[SkySkimmer]

The failing tests look kinda bad no?

< fun var : API.type -> Type =>
---
> fun var : type (Language.Compilers.base.type.type base) -> Type =>

-fun x : positive => (- Z.pos x~0 + 0)%Z
+fun x : positive => (- Zpos x~0 + 0)%Z

[SkySkimmer]

Not sure we want this change

[JasonGross]

I think this is a bad idea, and seems to me to be removing a feature rather than fixing a bug. At the very least, it should be possible to indicate at declaration time whether am abbreviation is meant to escape the scope of the module. (Note that an abbreviation whose printing does not escape the module scope is already possible to emulate by having an only parsing abbreviation + an only printing notation that is not an abbreviation.)

[proux01]

Note that an abbreviation whose printing does not escape the module scope is already possible to emulate by having an only parsing abbreviation + an only printing notation that is not an abbreviation.

That's definitely not an acceptable workaround.

That being said, the fix indeed seem more complicated than initially expected. We may need to think a bit more about this whole abbreviation locality story.

[SkySkimmer]

Rocq call: try having standard local/export/global behaviours for the printing rule (with export as default, and current behaviour is close to global)

[proux01]

if all that is needed is replacing Notation with #[global] Notation or Global Notation, and then there are no diffs, I'm happy to merge an overlay making this change, and have no objection.

CI confirms this is indeed the case
@JasonGross please merge the rewriter and fiat-crypto overlays and update your review status here

[JasonGross]

Have not looked at code changes, but the behavior change seems good

[proux01]

@coqbot merge now

[coqbot-app]

@proux01: Please take care of the following overlays:

• 20816-SkySkimmer-abbrev-mode.sh