Skip to Content.
Sympa Menu

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

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



Archive powered by MHonArc 2.6.18.

Top of Page