Builder instances must always depend on their factory - deprecate HB.instance K F.

[CohenCyril]

This is enforced by HB.instance Definition _ := _ via a let in hack, but it does not work for the "existing instance command" HB.instance T F, as spotted by @proux01.

Here is a minmal counter example:

From HB Require Import structures.

HB.mixin Record hasInvol T := { invol : T -> T }.
HB.structure Definition Invol := { T of hasInvol T }.

HB.factory Record mkIdInvol T := { }.
HB.builders Context T of mkIdInvol T.
Definition XXX := hasInvol.Build T id.
HB.instance T XXX.
HB.end.

HB.instance Definition _ := mkIdInvol.Build nat.

[gares]

Do we have any reason to keep the existing instance command? It seems to be subsumed by the other one even if the instance already has a name.

[CohenCyril]

Yes we can deprecate it.