blob: a111a045f0dfd5bcf4fb390f10a1f618ab310355 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
Require Export Crypto.Util.FixCoqMistakes.
(** find the head of the given expression, underneath [fun] and [forall] *)
Ltac head_under_binders_gen redtac expr :=
let expr := redtac expr in
match expr with
| ?f _ => head_under_binders_gen redtac f
| fun x : ?T => @?f x
=> lazymatch constr:(fun x : T
=> ltac:(let f' := (eval cbv beta in (f x)) in
let h := head_under_binders_gen redtac f' in
exact h)) with
| fun _ => ?f => f
| ?f => f
end
| forall x, @?f x
=> head_under_binders_gen redtac f
| ?expr => expr
end.
Ltac head_under_binders expr := head_under_binders_gen ltac:(fun e => e) expr.
Ltac head_hnf_under_binders expr := head_under_binders_gen ltac:(fun e => eval hnf in e) expr.
|
