From 7ea8a55692e2a2d32efa0c84e19c37a3b56a0fd1 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 19 Aug 2011 09:13:09 +0000 Subject: Cleaned up old commented-out parts git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1719 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 21 --------------------- 1 file changed, 21 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index 3948640..f18c091 100644 --- a/common/Events.v +++ b/common/Events.v @@ -1044,18 +1044,6 @@ Proof. intros. inv H. inv H1. inv H13. inv H14. inv H10. inv H11. exploit Mem.loadbytes_length; eauto. intros LEN. -(* - destruct (zle sz 0). - (* empty copy *) - rewrite nat_of_Z_neg in LEN; auto. - assert (bytes = nil). destruct bytes; simpl in LEN; congruence. - subst. rewrite Mem.storebytes_empty in H8. inv H8. - exists Vundef; exists m1'. - split. econstructor; eauto. rewrite Mem.loadbytes_empty; eauto. - apply Mem.storebytes_empty. - split. constructor. split. auto. red; auto. - (* nonempty copy *) -*) exploit Mem.loadbytes_extends; eauto. intros [bytes2 [A B]]. exploit Mem.storebytes_within_extends; eauto. intros [m2' [C D]]. exists Vundef; exists m2'. @@ -1079,15 +1067,6 @@ Proof. (* injections *) intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. exploit Mem.loadbytes_length; eauto. intros LEN. -(* - destruct (zle sz 0). - (* empty copy *) - rewrite nat_of_Z_neg in LEN; auto. - assert (bytes = nil). destruct bytes; simpl in LEN; congruence. - subst. rewrite Mem.storebytes_empty in H9. inv H9. - exists f; exists Vundef; exists m1'. - split. econstructor; eauto. -*) assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty). -- cgit v1.2.3