Make some tactics a bit more powerful

2 files changed, 7 insertions, 3 deletions

diff --git a/src/Util/Tactics/MoveLetIn.v b/src/Util/Tactics/MoveLetIn.v
index c5ec3d8a8..32959d716 100644
--- a/src/Util/Tactics/MoveLetIn.v
+++ b/src/Util/Tactics/MoveLetIn.v
@@ -46,7 +46,7 @@ Local Ltac with_uconstr_in_goal uc k :=
     of the form [lhs = rhs]. *)
 Ltac context_to_dlet_in_rhs f :=
   lazymatch goal with
-  | [ |- ?LHS = ?RHS ]
+  | [ |- ?R ?LHS ?RHS ]
     => with_uconstr_in_goal
          f
          ltac:(fun f
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.