coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] eauto loops

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] eauto loops
Date: Mon, 27 Jun 2016 16:13:10 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f54.google.com
Ironport-phdr: 9a23:ICnhrxd/NXFQqj8xO1FtX5DvlGMj4u6mDksu8pMizoh2WeGdxc64YR7h7PlgxGXEQZ/co6odzbGH6+a5AydZvt6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JXvkbnosMSMKyxzxxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cY6Lod8JtLVry/dKAlR5RZCi4nOiY7/p7Frx7GGDWG6noZGlcflhtWCkCR8gPzWpbvuwPxs/c71SWHa56lBYsoUCivuv84ACTjjz0KYmY0

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

[Coq-Club] eauto loops, Vadim Zaliva, 06/27/2016
- Re: [Coq-Club] eauto loops, Matthieu Sozeau, 06/27/2016
  - Re: [Coq-Club] eauto loops, Vadim Zaliva, 06/28/2016
    - Re: [Coq-Club] eauto loops, Matthieu Sozeau, 06/28/2016
      - Re: [Coq-Club] eauto loops, Vadim Zaliva, 06/28/2016