blob: 5f7772578d3e97a670296848b997dc60752506fe (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Require Import Crypto.Util.Tactics.ChangeInAll.
(** fully reduces the first argument to [t], wherever it appears *)
Ltac unfold_first_arg t :=
repeat match goal with
| [ H : context[t ?x] |- _ ] => progress change_with_compute_in_all x
| [ |- context[t ?x] ] => progress change_with_compute_in_all x
end.
(* use uconstr so we can have underscores *)
Tactic Notation "unfold_first_arg" uconstr(t) := unfold_first_arg t.
|
