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/Deadcodeproof.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'backend/Deadcodeproof.v') diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index 26953479..a8d79c3f 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -168,8 +168,7 @@ Proof. + subst b0. apply SETN with (access := fun ofs => Mem.perm m1' b ofs Cur Readable /\ Q b ofs); auto. intros. destruct H5. eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - apply H1; auto. -+ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. apply H1; auto. ++ eapply ma_memval; eauto. eapply Mem.perm_storebytes_2; eauto. - rewrite (Mem.nextblock_storebytes _ _ _ _ _ H0). rewrite (Mem.nextblock_storebytes _ _ _ _ _ ST2). eapply ma_nextblock; eauto. @@ -551,7 +550,7 @@ Proof. intros. exploit analyze_successors; eauto. rewrite ANPC; simpl. intros [A B]. econstructor; eauto. eapply eagree_ge; eauto. - eapply magree_monotone; eauto. intros; apply B; auto. + eapply magree_monotone; eauto. Qed. (** Builtin arguments and results *) @@ -1134,5 +1133,3 @@ Proof. Qed. End PRESERVATION. - - -- cgit