blob: 2e4008ae565b29204dce19afef18fbbeb686c6f5 (
plain)
1
2
3
4
5
6
7
8
9
|
(* show alternating separators in typeclass debug output; see discussion in PR #868 *)
Parameter foo : Prop.
Axiom H : foo -> foo.
Hint Resolve H : foo.
Goal foo.
Typeclasses eauto := debug.
Fail typeclasses eauto 5 with foo.
Abort.
|