From b2bd8ee27df8daa18b4fffcc688f831462c018bb Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 8 Dec 2023 19:08:19 -0500 Subject: [PATCH] Fix unfolding of let in rewrite rule proving Fixes the issue blocking https://github.com/mit-plv/fiat-crypto/pull/1780 --- src/Rewriter/Rewriter/ProofsCommonTactics.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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