The Coq mailing list

[James Lottes <jlottes AT gmail.com>]

Since nobody's mentioned it yet: you can trace through typeclass
resolution interactively with "Set Ltac Debug." in coqtop (though it's
not necessarily obvious which instances/hints are being triggered).
When I get stuck trying to figure out why typeclass resolution isn't
working as I expect, I often resort to pasting my whole development
into coqtop, up to just before the slow command, then "Set Ltac
Debug," followed by the problematic command (a rewrite in your case).
This can be pretty painful, but I haven't found a better way to debug
typeclass resolution.

Cheers,
James

On Mon, Nov 30, 2015 at 9:22 PM, Vadim Zaliva 
<vzaliva AT cmu.edu>
 wrote:
>
> On Nov 30, 2015, at 18:57 , Vadim Zaliva 
> <vzaliva AT cmu.edu>
>  wrote:
>
> Any hints how to analyze the debug log? What should I look for? Here is
> partial log file:
>
> http://bit.ly/1St2sZy
>
>
> Here is a digest of a bigger log file, which shows the search tree:
>
> http://bit.ly/1LK8n6Q
>
>
> Sincerely,
> Vadim Zaliva
>
> --
> CMU ECE PhD candidate
> Mobile: +1(510)220-1060
> Skype: vzaliva
>