test-suite/bugs/closed/bug_5093.v


1
2
3
4
5
6
7
8
9
10
11
12

Axiom P : nat -> Prop.
Axiom PS : forall n, P n -> P (S n).
Axiom P0 : P 0.

Hint Resolve PS : foobar.
Hint Resolve P0 : foobar.

Goal P 100.
Proof.
Fail typeclasses eauto 100 with foobar.
typeclasses eauto 101 with foobar.
Abort.