The Coq mailing list

[Gregory Malecha <(e29315a54f%hidden_head%e29315a54f)gmalecha(e29315a54f%hidden_at%e29315a54f)eecs.harvard.edu(e29315a54f%hidden_end%e29315a54f)>]

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.

Thank you.

--
gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/