The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Vadim,

  no, they are different currently, typeclasses eauto has the ability to backtrack more on dependent goals, i.e. goals

that depend on each other. I'd be curious to understand how you got the trace above though!

Best regards,

-- Matthieu

On Tue, Jun 28, 2016 at 1:13 AM Vadim Zaliva <vzaliva AT cmu.edu> wrote:

On Mon, Jun 27, 2016 at 10:14 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

  could you give a bit more context about this? Are you calling eauto or 

typeclasses eauto for example?

Sorry, I am still learning typeclass resolution. I was now aware of typeclass eauto, and it is very helpful. Another advice, given earlier in this list was to use "Set Ltac Debug" to trace "typeclass eauto" which is also very helpful.

Using these two techniques I was able to move past this problem, and now continuing to debug my code.

One related question: is "typeclass eauto" just "eauto with typelcasses_instances" plus additional debug output?

--

CMU ECE PhD candidate

Mobile: +1(510)220-1060