blob: 6de8324641e8efd2b3b420c8435178bc44809171 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
|
Class A (X : Type) := {}.
Hint Mode A ! : typeclass_instances.
Class B X {aX: A X} Y := { opB: X -> Y -> Y }.
Hint Mode B - - ! : typeclass_instances.
Section Section.
Context X {aX: A X} Y {bY: B X Y}.
(* Set Typeclasses Debug. *)
Let ok := fun (x : X) (y : Y) => opB x y.
Let ok' := fun x (y : Y) => opB x y.
End Section.
|
