The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

Thank you. Hints that aren't associated with a name go in the [core] database.

Parameter bla : forall m : nat, m = m.

Print HintDb core.

Hint Resolve bla.

Print HintDb core.

Remove Hints bla.

Print HintDb core.

On Thu, Feb 27, 2014 at 11:01 PM, Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

On 27/02/2014 23:53, Jason Gross wrote:
> I believe it was requested and might be planed, but not yet implemented.

In trunk, there is an undocumented command (that one should not use):

%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

Parameter bla : forall m : nat, m = m.

Hint Resolve bla : foo.

Print HintDb foo.

Remove Hints bla : foo.

Print HintDb foo.

%< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %< %<

This only works with hints associated to a name, and I personnally find
it dangerous to use, but at least it's here to hack around.

PMP