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: Catalin Hritcu <catalin.hritcu AT gmail.com>
- To: Tom Prince <tom.prince AT ualberta.net>
- Cc: 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 20:55:49 -0400
On Sat, Oct 13, 2012 at 7:37 PM, Tom Prince
<tom.prince AT ualberta.net>
wrote:
> 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.
>
Thanks Tom, this is indeed very useful for diagnosing the problem.
Print HintDb shows indeed big differences between "core" and newly
created hint databases.
Print HintDb core.
(* Non-discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: none
... *)
Create HintDb mydb.
Print HintDb mydb.
(* Non-discriminated database
Unfoldable variable definitions: all
Unfoldable constant definitions: all
... *)
This also shows that Jason's trick works:
Hint Transparent one.
Print HintDb core.
(* Non-discriminated database
Unfoldable variable definitions: none
Unfoldable constant definitions: one
... *)
The main remaining questions: (1) why are the defaults for "core" set
this way and (2) is there any way to change them?
Thanks,
Catalin
- [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.