aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_12970.v
blob: 69ce7ec2c283f594f1741f9d32ab1a55ccfafc7a (plain)
1
2
3
4
Arguments existT _ & _ _.

Definition f := fun X (A : X -> Type) (P : forall x, A x -> Type) x y =>
        existT (fun f => forall x, P x (f x)) x y : sigT (fun f => forall x, P x (f x)).