HB does not preserve the name of implicit arguments

[silene]

From HB Require Import structures.

HB.mixin Record IsAddComoid A := { zero : A }.
HB.structure Definition AddComoid := { A of IsAddComoid A }.

About zero.
(* zero : forall {s : AddComoid.type}, s *)

Note how the implicit argument of zero is named s instead of A. This makes it a bit tedious to port developments. Here is an example of an actual modification I had to make to avoid depending on the automatically generated identifier:

-change Rmult with (scal (V := R)).
+change Rmult with (@scal _ R).

(I could also have written Arguments scal K V : rename. But I do not want to perform such a command for all the symbols of the hierarchy.)

[gares]

I see your point, but both A in your directives denote the carrier of what HB called s, eg AddComoid.sort s, so it not really about preserving a name, but rather using one as a good default.

I don't if we have a better pattern for writing @scal _ R in mathcomp, since we surely don't rely on the s name. I suspect R should be inferred by a CS inference if you unify Rmult with @scal _ _ (and change should do it). Does rewrite -[Rmult]/(@scal) work?

[CohenCyril]

We must indeed honor the name given by HB.structure

[CohenCyril]

Actually naming is not really stable by operator transfer from one structure to another :-/ so I'm not sure how to handle this in a backward compatible way...

[gares]

Let's first see if the use case for making the name part of the "API" is motivated by the tactic language or not.

[silene]

No, using rewrite -[Rmult]/scal (as well as @scal variants) does not work any better than change Rmult with (@scal _ R), since the "fold pattern scal does not match redex Rmult". I have to use rewrite -[Rmult]/(@scal _ R).

That said, you are at least right that, e.g., rewrite -[Rminus]/minus works better than change Rminus with minus. But in the case of scal, the relation with Rmult is not that canonical.