The Coq mailing list

[Tom Prince <tom.prince AT ualberta.net>]

On Fri, 23 Dec 2011 10:53:28 -0800, Michael Shulman 
<mshulman AT ucsd.edu>
 wrote:
> >> Hint Resolve @some_method.
> > You probably want to add ': typeclass_instances' here.
> Why?

Typeclass resolution uses the typeclass_instances hint db.

> >> I am told "some_method cannot be used as a hint".  Is there a way to
> >> do this?
> >
> > Is is that some_method cannot be used as a hint by *auto*?
> 
> I'm not sure -- are you asking me?  This shouldn't cause the "Hint
> Resolve" command to fail, should it?  The manual says that if a hint
> will only be used by eauto, then "Hint Resolve" just prints a warning.

I wasn't sure what you were seeing. It looks like this caused by having
a bad head contatnt. Either a forall, or bound variable, it looks like,
from the source.

> > There are a number of other things one can do. The simplest method is to 
> > use
> > ':>' instead of ':' when declaring the projection ... this automatically
> > declares a hint for the projection.
> 
> The method in question isn't a projection declared as part of the
> typeclass definition, but a function defined later which happens to
> take an argument belonging to a typeclass.  (Is the word "method"
> wrong in this context?)

I don't know if there is standard terminology for this.

  Tom