test-suite/success/polymorphism.v


1
2
3
4
5
6
7
8
9
10
11
12

(* Some tests of sort-polymorphisme *)
Section S.
Variable A:Type.
(*
Definition f (B:Type) := (A * B)%type.
*)
Inductive I (B:Type) : Type := prod : A->B->I B.
End S.
(*
Check f nat nat : Set.
*)
Check I nat nat : Set.