The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

Is there a good way to make [trivial] (or [eauto 1]) print out what it's trying as/before it's trying it?  I recently had a case where [trivial] took forever (over 10s).  I made a lucky guess and it was instantaneous once I cleared a hypothesis that it was taking forever trying to unify with the goal, but I'd like a more systematic way of debugging this.

Thanks,

Jason