blob: fa7a301d6164d971ab9267a7ee52fc6977df2112 (
plain)
1
2
3
4
5
6
7
8
9
10
|
Require Export Crypto.Util.FixCoqMistakes.
(** find the head of the given expression *)
Ltac head expr :=
match expr with
| ?f _ => head f
| _ => expr
end.
Ltac head_hnf expr := let expr' := eval hnf in expr in head expr'.
|