diff options
Diffstat (limited to 'backend/Inliningspec.v')
| -rw-r--r-- | backend/Inliningspec.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v index 23770cb7..f56d6d18 100644 --- a/backend/Inliningspec.v +++ b/backend/Inliningspec.v @@ -512,7 +512,7 @@ Proof. assert (dstk ctx + mstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. omega. intros. simpl in H. rewrite S1. - transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. + transitivity (s1.(st_code)!pc0). eapply set_instr_other; eauto. unfold node in *; xomega. eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. red; simpl. subst s2; simpl in *. xomega. red; simpl. split. auto. apply align_le. apply min_alignment_pos. @@ -542,7 +542,7 @@ Proof. assert (dstk ctx <= dstk ctx'). simpl. apply align_le. apply min_alignment_pos. omega. omega. intros. simpl in H. rewrite S1. - transitivity s1.(st_code)!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. + transitivity (s1.(st_code))!pc0. eapply set_instr_other; eauto. unfold node in *; xomega. eapply add_moves_unchanged; eauto. unfold node in *; xomega. xomega. red; simpl. subst s2; simpl in *; xomega. |