aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4782.v
blob: ed44437861b95d3c7a56ffcedb692368c1ca1e35 (plain)
1
2
3
4
5
6
7
8
9
(* About typing of with bindings *)

Record r : Type := mk_r { type : Type; cond : type -> Prop }.

Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.

Goal p.
Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.