diff --git a/src/Rewriter/Rewriter/ProofsCommonTactics.v b/src/Rewriter/Rewriter/ProofsCommonTactics.v
index dffb266c2..10ed407f3 100644
--- a/src/Rewriter/Rewriter/ProofsCommonTactics.v
+++ b/src/Rewriter/Rewriter/ProofsCommonTactics.v
@@ -535,8 +535,8 @@ Module Compilers.
                      | try reflexivity ]
                 | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ]
                   => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh; cbv beta; intros
-                | [ |- expr.interp_related_gen _ _ (expr.LetIn ?v ?f) (LetIn.Let_In ?V ?F) ]
-                  => rewrite (LetIn.unfold_Let_In V F);
+                | [ |- expr.interp_related_gen _ _ (expr.LetIn ?v ?f) (@LetIn.Let_In ?A ?B ?V ?F) ]
+                  => rewrite (@LetIn.unfold_Let_In A B V F);
                      let vh := fresh in
                      set (vh := v);
                      let fh := fresh in