From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Fri, 22 Sep 2017 19:50:52 +0200 Subject: Remove coq warnings (#28) Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts. --- common/Events.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'common/Events.v') diff --git a/common/Events.v b/common/Events.v index ab804aa7..63922bc5 100644 --- a/common/Events.v +++ b/common/Events.v @@ -999,7 +999,7 @@ Proof. assert (SZ: v2 = Vptrofs sz). { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. } subst v2. - exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl. intros [m3' [A B]]. exploit Mem.store_within_extends. eexact B. eauto. eauto. intros [m2' [C D]]. @@ -1011,11 +1011,11 @@ Proof. assert (SZ: v' = Vptrofs sz). { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. } subst v'. - exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_parallel_inject; eauto. apply Z.le_refl. apply Z.le_refl. intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]]. exploit Mem.store_mapped_inject. eexact A. eauto. eauto. instantiate (1 := Vptrofs sz). unfold Vptrofs; destruct Archi.ptr64; constructor. - rewrite Zplus_0_r. intros [m2' [E G]]. + rewrite Z.add_0_r. intros [m2' [E G]]. exists f'; exists (Vptr b' Ptrofs.zero); exists m2'; intuition auto. econstructor; eauto. econstructor. eauto. auto. @@ -1206,7 +1206,7 @@ Proof. assert (RPSRC: Mem.range_perm m1 bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sz) Cur Nonempty). eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty). - replace sz with (Z_of_nat (length bytes)). + replace sz with (Z.of_nat (length bytes)). eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. rewrite LEN. apply nat_of_Z_eq. omega. assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty). -- cgit