The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm not sure what's going on, exactly, but note that the following works, too:

Hint Transparent one.

Hint Constructors prev.

Lemma prev_one_zero'''' : prev one zero.

Proof.

  debug eauto.

Qed.

On Thu, Oct 11, 2012 at 9:07 AM, Catalin Hritcu <catalin.hritcu AT gmail.com> wrote:

OK, I've simplified the test illustrating the problem even further:

Inductive prev : nat -> nat -> Prop :=
  | previous : forall n, prev (S n) n.

Definition zero := O.
Definition one := S O.

(* This works *)
Lemma prev_one_zero : prev one zero.
Proof.
  eauto using prev.

Qed.

(* This also works *)

Lemma prev_one_zero' : prev one zero.
Proof.
  eauto using previous.

Qed.

(* This also works *)
Create HintDb mydb.

Hint Constructors prev : mydb.
Lemma prev_one_zero'' : prev one zero.

Proof.
  eauto with mydb.
Qed.

(* But this doesn't work! *)

Hint Constructors prev.
Lemma prev_one_zero''' : prev one zero.
Proof.
  eauto.
Abort.

(* Adding [core] explicitly doesn't help either *)
Lemma prev_one_zero''' : prev one zero.
Proof.
  eauto with core.
Abort.

(* Neither does this *)
Hint Resolve previous.
Lemma prev_one_zero''' : prev one zero.
Proof.
  eauto.
Abort.

(* Unfolding [one] makes it work though *)
Lemma prev_one_zero''' : prev one zero.
Proof.
  unfold one. eauto.
Qed.