aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3542.v
blob: b6837a0c334913399dc248872bf9c9abd894a371 (plain)
1
2
3
4
5
6
Section foo.
  Context {A:Type} {B : A -> Type}.
  Context (f : forall x, B x).
  Goal True.
    pose (r := fun k => existT (fun g => forall x, f x = g x)
                               (fun x => projT1 (k x)) (fun x => projT2 (k x))).