[classifier] visibility on attributes

[gares]

The vernac classifier did thread around attributes for but was not passing them to custom classifiers (indeed attributes were added after custom classifiers).

Thanks to this a plugin can define a command that opens a proof depending on an attribute, like #[program] or #[refine].

This PR unblocks LPCIC/coq-elpi#831 and HB 2.0

overlay

• adapt to rocq-prover/rocq#20839 LPCIC/coq-elpi#845
• Adapt to rocq-prover/rocq#20839 (classifier sees ~atts) MetaRocq/metarocq#1191

[gares]

Now it looks to simple that I wonder if it could target 9.1

[SkySkimmer]

It looks like elpi needs an overlay which is kinda annoying to get in 9.1 but still somewhat possible if done quick I guess.
You will need to provide a 9.1-compatible elpi commit with the overlay.

[gares]

It will land shortly.

BTW, I do have a recurrent problem with

        if ! git config get --local commit.template; then
          git config set --local commit.template "$template_file"
        fi

apparently my git version (2.43) does not have these commands

[SkySkimmer]

BTW, I do have a recurrent problem with

speak on zulip, this isn't the right place

[gares]

@coqbot run full ci

[gares]

Looks good to me.

[SkySkimmer]

@coqbot merge now

@gares I let you make the backport PR

[coqbot-app]

@SkySkimmer: Please take care of the following overlays:

• 20839-gares-vernac-class-atts.sh

[gares]

I'll do it tomorrow