diff options
| author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2017-09-22 19:50:52 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-09-22 19:53:06 +0200 |
| commit | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (patch) | |
| tree | 3ffd8bcb28a88ae4ff51989aed37b0ad2cb676b2 /common/Events.v | |
| parent | 0f210f622a4609811959f4450f770c61f5eb6532 (diff) | |
| download | compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.tar.gz compcert-kvx-8d5c6bb8f0cac1339dec7b730997ee30b1517073.zip | |
Remove coq warnings (#28)
Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.
Diffstat (limited to 'common/Events.v')
| -rw-r--r-- | common/Events.v | 8 |
1 files changed, 4 insertions, 4 deletions
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). |