Make some tactics a bit more powerful

1 files changed, 6 insertions, 2 deletions

diff --git a/src/Util/Tactics/UnfoldArg.v b/src/Util/Tactics/UnfoldArg.v
index 5f7772578..68d35cff4 100644
--- a/src/Util/Tactics/UnfoldArg.v
+++ b/src/Util/Tactics/UnfoldArg.v
@@ -7,5 +7,9 @@ Ltac unfold_first_arg t :=
          | [ |- 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.
+(** fully reduces the second argument to [t], wherever it appears *)
+Ltac unfold_second_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.