diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2016-07-08 14:43:57 +0200 |
| commit | e73d5db97cdb22cce2ee479469f62af3c4b6264a (patch) | |
| tree | 035d31018c2abec698eb49a205c60bbf5c24ba0d /backend/Inliningspec.v | |
| parent | db2445b3b745abd1a26f5a832a29ca269c725277 (diff) | |
| download | compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.tar.gz compcert-kvx-e73d5db97cdb22cce2ee479469f62af3c4b6264a.zip | |
Port to Coq 8.5pl2
Manual merging of branch jhjourdan:coq8.5.
No other change un functionality.
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. |