test-suite/bugs/2428.v


1
2
3
4
5
6
7
8
9
10

Axiom P : nat -> Prop.

Definition myFact := forall x, P x.

Hint Extern 1 (P _) => progress (unfold myFact in *).

Lemma test : (True -> myFact) -> P 3.
Proof. 
  intros. debug eauto.
Qed.