The Coq mailing list

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

On 2011-02-18, Aaron Bohannon wrote:
> On Mon, Feb 14, 2011 at 9:20 PM, Tom Prince 
> <tom.prince AT ualberta.net>
>  wrote:
> > I don't know whether this behaviour is expected, but the typeclass
> > mechanism still has kinks and oddities in it. It would probably help if
> > you gave a small self contained example of this behavior (and the
> > behviour of auto) occurring.
> 
> I've given an example below of the behaviors I was describing
> regarding apply, auto, and type classes.  As I said, I'm not sure if
> they are "bugs," but I want to wrap my head around what is going on so
> that I can use the proper work-arounds.
> 
>  - Aaron

This is probably worth a bug report, even though the behaviour is
currently expected. What is going on is, is that the contr label
indicates that the paramater is to be a coq term. This triggers implicit
argument handling and thus typeclass resolution.

  Tom