The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi Catalin,

On 13 oct. 2012, at 20:55, Catalin Hritcu 
<catalin.hritcu AT gmail.com>
 wrote:
> <snip/>
> The main remaining questions: (1) why are the defaults for "core" set
> this way and (2) is there any way to change them?

1) Because of backwards compatibility issues (too many goals are solved
if we set transparency for core, and sometimes it might take too much
time or even diverge in some cases).
2) No, these settings are set at creation time. One can build Hint databases
with transparent variables/constants only using [Create HintDb], other
databases have opaque variables/constants by default (see 1).

Best,
-- Matthieu