From e73d5db97cdb22cce2ee479469f62af3c4b6264a Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Fri, 8 Jul 2016 14:43:57 +0200 Subject: Port to Coq 8.5pl2 Manual merging of branch jhjourdan:coq8.5. No other change un functionality. --- backend/Inliningspec.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/Inliningspec.v') 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. -- cgit