The Coq mailing list

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

I've run into some inconsistent behavior with Coq 8.4, in which hints
in "core" are ignored by eauto, but the same hints added to a
different hint database or directly with the "using" clause work just
fine. I've attached a small bit of a larger development where this
problem was quite pervasive. Here are the most interesting bits:

(* This works *)
Lemma red1_t : exists t', red1 tt t'.
Proof.
  eauto using red1.
Qed.

(* This also works *)
Lemma red1_t'' : exists t', red1 tt t'.
Proof.
  eauto using red1_beta.
Qed.

(* This also works *)
Create HintDb mydb.
Hint Constructors red1 : mydb.
Lemma red1_t' : exists t', red1 tt t'.
Proof.
  eauto with mydb.
Qed.

(* But this doesn't work! *)
Hint Constructors red1.
Lemma red1_t''' : exists t', red1 tt t'.
Proof.
  eauto.
Abort.

(* Unfolding tt makes it work though *)
Lemma red1_t''' : exists t', red1 tt t'.
Proof.
  unfold tt. debug eauto.
Qed.

(* But not with Hint Unfold? *)
Hint Unfold tt.
Lemma red1_t'''' : exists t', red1 tt t'.
Proof.
  debug eauto.
Abort.

(* Still no luck *)
Lemma red1_t''''' : exists t', red1 tt t'.
Proof.
  debug eauto with core.
Abort.

(* But if we use a database that's not core it all works *)
Hint Unfold tt : mydb.
Lemma red1_t'''' : exists t', red1 tt t'.
Proof.
  debug eauto with mydb.
Qed.

Attachment: Strange.v
Description: Binary data