aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3249.v
blob: 71d457b002ec536be71fee3d691cf032f61d2130 (plain)
1
2
3
4
5
6
7
8
9
10
11
Set Implicit Arguments.

Ltac ret_and_left T :=
  let t := type of T in
  lazymatch eval hnf in t with
    | ?a /\ ?b => constr:(proj1 T)
    | forall x : ?T', @?f x =>
      constr:(fun x : T' => ltac:(let fx := constr:(T x) in
                              let t := ret_and_left fx in
                              exact t))
  end.