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.
|
