blob: 0aabf80c8a78edd584799cd8f59fb051af255610 (
plain)
1
2
3
4
5
6
|
(** Execute [progress tac] on all subterms of the goal. Useful for things like [ring_simplify]. *)
Ltac tac_on_subterms tac :=
repeat match goal with
| [ |- context[?t] ]
=> progress tac t
end.
|