aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/TypeclassDebug.v
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.