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: Tue, 28 Jun 2016 08:22:45 -0700
Authentication-results: mail3-smtp-sop.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:nvykYhR3qaB4zXGxJ4RGabkxW9psv+yvbD5Q0YIujvd0So/mwa64ZhGN2/xhgRfzUJnB7Loc0qyN4vimADdLsc/JmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYsExnyfTB4Ov7yUtaLyZ/mj6broNaDOk1hv3mUWftKNhK4rAHc5IE9oLBJDeIP8CbPuWZCYO9MxGlldhq5lhf44dqsrtY4q3wD86Fpy8kVWqLjOq88ULZwDTI8Mmlz6te4mwPESF6x73cdVy0kmx5JHQGNuA/oV5PwrCLSve9gniSWIJulHvgPRT2+4vIzG1fTgyAdOmth/Q==

On Tue, Jun 28, 2016 at 12:57 AM, Matthieu Sozeau <mattam AT mattam.org> wrote:

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,

I already changed my code they way this message is gone and I could not easily to get back the old version. However if it occurs again I will let you know.

I think the problem was in a cyclic hints. Something like A->B and B->A. One of them was class constructor and another was external hint I've introduced.

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