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/Deadcodeproof.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/Deadcodeproof.v')
| -rw-r--r-- | backend/Deadcodeproof.v | 7 |
1 files changed, 2 insertions, 5 deletions
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. - - |