HB.instance without Definition should take head symbol rather than fully applied term

[CohenCyril]

E.g.

Definition stuff  T  : mixin (f T) :=  ...
HB.instance f stuff.

instead of

Section stuff.
Variable T.
Definition stuff  : mixin (f T) :=  ...
HB.instance (f T) stuff.
End stuff.

[gares]

The more I think about it and the more I believe that we should stop supporting HB.instance f stuff.
The point is that you can always write HB.instance Definition foo params : factory params (f args) := stuff more_args.
Without that info I can surely turn f into a type by postulating all its arguments, but I've no idea on how to pass them to stuff.

We may want to provide something like HB.instance Definition _ params : factory params (hd args) := stuff more_args which does not really make a definition, but internally follows the same code path.

[gares]

I've pushed a commit implementing the latter. Unfortunately there is a bug in coq-elpi, fixed in master, which makes it fail, so I did not put a file in the test suite. But it works ;-)