The Coq mailing list

[Julien Tesson <julien.tesson AT lacl.fr>]

Le 28/02/2014 12:34, Matthieu Sozeau a écrit :

Because of a type unification, when applying the instance, Equiv and relation should be convertible.

Le vendredi 28 février 2014, Frédéric Blanqui <frederic.blanqui AT inria.fr> a écrit :

Hi. To better understand what's going on, could you explain why Equiv needs to be unfolded? Best regards, Frédéric.
 

Le 28/02/2014 02:59, Jason Gross a écrit :

You need to tell Coq that it's allowed to unfold [Equiv].  In this case, your example goes through if you do

Typeclasses Transparent Equiv.

-Jason

Great !

thanks to all for your answers !
So, just to better understand what's in going on there, is it just typeclasses that are opaque  for the unification during the instance search or is it the same for all terms ?
Is there some documentation on this somewhere ?
Cheers,
Julien