Remove coq warnings (#28)

Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.

4 files changed, 5 insertions, 5 deletions

diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v
index da444a4b..cc45a8de 100644
--- a/riscV/Asmgenproof.v
+++ b/riscV/Asmgenproof.v
@@ -920,7 +920,7 @@ Local Transparent destroyed_by_op.
   generalize EQ; intros EQ'. monadInv EQ'.
   destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0.
   unfold store_stack in *.
-  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
+  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros [m1' [C D]].
   exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto.
   intros [m2' [F G]].
diff --git a/riscV/Conventions1.v b/riscV/Conventions1.v
index ff993650..df7ddfd2 100644
--- a/riscV/Conventions1.v
+++ b/riscV/Conventions1.v
@@ -420,7 +420,7 @@ Proof.
              ofs + typesize ty <= max_outgoing_2 n p).
   { intros. destruct p; simpl in H; intuition; subst; simpl.
   - xomega.
-  - eapply Zle_trans. 2: apply A. xomega.
+  - eapply Z.le_trans. 2: apply A. xomega.
   - xomega. }
   assert (C: forall l n,
              In (S Outgoing ofs ty) (regs_of_rpairs l) ->
@@ -428,7 +428,7 @@ Proof.
   { induction l; simpl; intros.
   - contradiction.
   - rewrite in_app_iff in H. destruct H.
-  + eapply Zle_trans. eapply B; eauto. apply Zge_le. apply fold_max_outgoing_above.
+  + eapply Z.le_trans. eapply B; eauto. apply Z.ge_le. apply fold_max_outgoing_above.
   + apply IHl; auto.
   }
   apply C. 
diff --git a/riscV/Op.v b/riscV/Op.v
index ae5a1017..bb04f786 100644
--- a/riscV/Op.v
+++ b/riscV/Op.v
@@ -1194,7 +1194,7 @@ Remark weak_valid_pointer_no_overflow_extends:
   Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
   0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 Proof.
-  intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2.
+  intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
 Qed.
 
 Remark valid_different_pointers_extends:
diff --git a/riscV/Stacklayout.v b/riscV/Stacklayout.v
index ba116380..d0c6a526 100644
--- a/riscV/Stacklayout.v
+++ b/riscV/Stacklayout.v
@@ -139,7 +139,7 @@ Proof.
   set (ostkdata := align (ol + 4 * b.(bound_local)) 8).
   assert (0 < w) by (unfold w; destruct Archi.ptr64; omega).
   replace (align_chunk Mptr) with w by (rewrite align_chunk_Mptr; auto).
-  split. apply Zdivide_0.
+  split. apply Z.divide_0_r.
   split. apply align_divides; omega.
   split. apply align_divides; omega.
   split. apply align_divides; omega.