Fix unfolding of let in rewrite rule proving

Fixes the issue blocking mit-plv/fiat-crypto#1780
JasonGross · Dec 9, 2023 · b2bd8ee · b2bd8ee
1 parent 3a0a5f7
commit b2bd8ee
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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