The Coq mailing list

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

> 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 ?
One should always read the documentation *before* asking such question, 
sorry. 
I just notice that the answer is almost in section 19.6.5 
(http://coq.inria.fr/refman/Reference-Manual022.html#sec678).
So if I understood right the documentation, The command for making term 
transparent or opaque works on any term.

But the default status of a given term is not clear to me. I guess it depends 
on some black magic made by some great magician in such a way that most of 
the time, we don't have to care about it. I'm I right ?

Cheers,
Julien