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?
Chronological Thread
- 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
- Re: [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/14/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
- [Coq-Club] Re: Why does eauto treat "core" differently than the other hint databases?, Catalin Hritcu, 10/11/2012
Archive powered by MHonArc 2.6.18.