Skip to content

Commit

Permalink
Fix unfolding of let in rewrite rule proving
Browse files Browse the repository at this point in the history
Fixes the issue blocking mit-plv/fiat-crypto#1780
  • Loading branch information
JasonGross committed Dec 9, 2023
1 parent 3a0a5f7 commit b2bd8ee
Showing 1 changed file with 2 additions and 2 deletions.
4 changes: 2 additions & 2 deletions src/Rewriter/Rewriter/ProofsCommonTactics.v
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit b2bd8ee

Please sign in to comment.