TODO: Experiment with Hints in `derive.v`

[affeldt-aist]

@yosakaon made the following observation:

#2040 (comment)

This is about the following hint:

Hint Extern 0 (is_derive _ _ (fun x => _ *m _) _) => apply: is_derive_mulmx : typeclass_instances.

[yosakaon]

I don't know if it is the best course of action to add such a hint and if it might break (I don't think so) other developments but it works well in my current development. I can open a PR but I'd like to know if there is any "canonical" way to deal with such a problem (simple apply fails in harder goals -> use apply:). But unless this hint is in place afaik, typeclass inference will fail at solving such goals, which fails the objective of using is_derive in the first place and renders is_derive_mulmx pointless.

[yosakaon]

eapply is_derive_mulmx works as well in a compound goal.

[affeldt-aist]

Since PR #2017 seems inconclusive, shall we close this issue? (fyi: @CohenCyril )

[affeldt-aist]

ping @yosakaon

[yosakaon]

I think it's ok to close