aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/Notations2.v
blob: 0d5cc9e24ceffef019f5fe2a276b894ea1c03f3b (plain)
1
2
3
4
5
6
7
8
9
10
11
(**********************************************************************)
(* 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).

(* Test bug #2091 (variable le was printed using <= !) *)

Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x.