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