The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

On 07/06/2012 05:43 PM, J. Ian Johnson wrote:
> I am turning the finite map library into a typeclass and extending it to use 
> setoids. There are different properties about them that are registered as 
> immediate or for resolve, but I can't do that kind of hint registration with 
> typeclass members. For example:
>
> Class TC := { mem : forall x : Type, x = x}.
>
> Hint Immediate mem.
>
> Error: Cannot infer the implicit parameter TC of mem.
> Could not find an instance for "TC".
>    

The above runs without an error for me in Coq 8.4beta2.