The Coq mailing list

[St�phane Lescuyer <stephane.lescuyer AT inria.fr>]

On Fri, Jun 11, 2010 at 11:00 AM, Adam Koprowski
<adam.koprowski AT gmail.com>
 wrote:
>   Btw. is there any reasonable way to "debug" resolution to figure out
> what's going on, in cases such as this one?

You can change the parameters of the resolution using Typeclasses
eauto := ... (cf 18.5.5 in Ref. Manual), for instance changing the
depth to something small enough that the resolution fails in
reasonable time, and looking at the output to see what instances the
system is trying to find. If on the other hand you are certain that
the adequate instances are available in the context, you can also try
switching from depth-first search to breadth-first search using the
bfs flag.

Hope this helps,
S.
-- 
I'm the kind of guy that until it happens, I won't worry about it. -
R.H. RoY05, MVP06