aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/inductive2.v
blob: 827c6f9fad792a89ac8a24577bfab3491bec8bf9 (plain)
1
2
3
4
(* A check that sort-polymorphic product is not set too low *)

Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B.
Fail Check (fun (A:Prop) (B:Type) => (prod A B : Prop)).