aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/2428.v
blob: a4f587a58d2163ff73d6dbd7f055e796c828c5df (plain)
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.