blob: d38e2a50e42778dfd7527e83e4e53a94ae14cb44 (
plain)
1
2
3
4
5
6
7
8
|
(* 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.
|
