blob: 039771d5d5491fd22f0dcb541b5547a9090819d3 (
plain)
1
2
3
4
5
6
7
|
(**********************************************************************)
(* Test call to primitive printers in presence of coercion to *)
(* functions (cf bug #2044) *)
Inductive PAIR := P (n1:nat) (n2:nat).
Coercion P : nat >-> Funclass.
Check (2 3).
|