The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

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