The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Le 9 mai 2012 à 00:39, Gregory Malecha a écrit :

Hello --

I'm working in the Coq 8.4beta trying to use the [Remove Hints] vernacular command that is described in this post (http://permalink.gmane.org/gmane.science.mathematics.logic.coq.club/6947). But it does not seem to work. 

Remove Hints LabelMap.Raw.Proofs.L.PX.eqk_refl.

Print HintDb core.

Prints out:

For LabelMap.Raw.Proofs.L.PX.eqk ->   unfold LabelMap.Raw.Proofs.L.PX.eqk(level 4, id 0)

                                      apply LabelMap.Raw.Proofs.L.PX.eqk_refl(level 0, id 0)           <==== this is what we just "removed"

                                      apply LabelMap.Raw.Proofs.L.PX.eqk_sym ; trivial(level 1, id 0)

                                      eapply LabelMap.Raw.Proofs.L.PX.eqk_trans(level 3, id 0)

This seems to be added by by [Hint Resolve], is there something that I'm doing wrong? Is it likely that this will work in the upcoming 8.4 release? I noticed that it was not part of the 8.4 CHANGELOG.

Hi Gregory,

  indeed this was a bug, Hints Remove did not work for hints inside modules. 

This will be working in the upcoming 8.4 release.

Best,

-- Matthieu