Provide a way to give names to canonical instances

[CohenCyril]

e.g.

#[instances(suffix="_ring")]
HB.structure Definition Ring := {...}.
HB.instance Definition _ := Ring.Build Z ....
Check (Z : Ring.type).
(* output should be: Z_ring : Ring.type *)

[gares]

But why Z and not Zarith_Z (or something like that, which is what it uses today before __canonical__Bli_Bla)?

[gares]

#[instances(suffix="_ring")]
HB.structure Definition Ring := {...}.
#[name="Z"] (* or #[name(short)] *)
HB.instance Definition _ := Ring.Build Z ....
(* Z_ring, Z_zmod, Z_whatever *)

[gares]

Maybe using the short name of the key should be the default.
But IIRC somewhere the key is "T" or some other silly name if you don't include the enclosing module.

[CohenCyril]

Maybe using the short name of the key should be the default.

I agree

[proux01]

C.f. #463