coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?

From: Tom Prince <tom.prince AT ualberta.net>
To: Catalin Hritcu <catalin.hritcu AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?
Date: Sat, 13 Oct 2012 17:37:36 -0600

Catalin Hritcu
<catalin.hritcu AT gmail.com>
writes:

> OK, I've simplified the test illustrating the problem even further:

There are a number of properties of databases that affect how they get
used, besides just hints. 'Print HintDb <name>.' might give some useful
information on what exactly is going on.

Tom

[Coq-Club] Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/11/2012
- [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/11/2012
  - Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Jason Gross, 10/11/2012
    - Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/11/2012
      - Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/11/2012
        
        Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Jason Gross, 10/11/2012
        
        Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Tom Prince, 10/14/2012
        
        Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/14/2012
        
        Re: [Coq-Club] Why does eauto treat "core" differently than the other hint databases?, Matthieu Sozeau, 10/14/2012