diff options
Diffstat (limited to 'cfrontend/SimplExprproof.v')
| -rw-r--r-- | cfrontend/SimplExprproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v index b3c861e..9134e11 100644 --- a/cfrontend/SimplExprproof.v +++ b/cfrontend/SimplExprproof.v @@ -2166,9 +2166,9 @@ Proof. inv H7. inversion H3; subst. econstructor; split. left; apply plus_one. eapply step_internal_function. econstructor. - rewrite H5; rewrite H6; auto. - rewrite H5; rewrite H6. eapply alloc_variables_preserved; eauto. - rewrite H5. eapply bind_parameters_preserved; eauto. + rewrite H6; rewrite H7; auto. + rewrite H6; rewrite H7. eapply alloc_variables_preserved; eauto. + rewrite H6. eapply bind_parameters_preserved; eauto. eauto. constructor; auto. |