blob: 9b787867fc0953f074cd46fab462ff229e65f843 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Class C := {}.
Definition useC {c:C} := nat.
Inductive foo {a b : C} := CC : useC -> foo.
(* If TC search runs before parameter unification it will pick the
wrong instance for the first parameter.
useC makes sure we don't completely skip TC search.
*)
|
