The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Is it possible to declare a typeclass method as a hint?  When I say

Hint Resolve some_method.

if no instances have yet been declared, I get a "cannot infer implicit
parameter" error.  If some instances have been declared, then
apparently only the method applied to the first such instance is
declared as a hint.  I can specify which instance I want with

Hint Resolve (@some_method some_instance).

but I want the hint to apply to *all* instances.  However, if I write

Hint Resolve @some_method.

I am told "some_method cannot be used as a hint".  Is there a way to do this?

Thanks,
Mike