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, 13 insertions, 13 deletions

diff --git a/x86/Asmgenproof.v b/x86/Asmgenproof.v
index 6caf4531..38816fd2 100644
--- a/x86/Asmgenproof.v
+++ b/x86/Asmgenproof.v
@@ -825,7 +825,7 @@ Transparent destroyed_by_jumptable.
   destruct (zlt Ptrofs.max_unsigned (list_length_z (fn_code x0))); inv EQ1.
   monadInv EQ0. rewrite transl_code'_transl_code in EQ1.
   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/x86/Conventions1.v b/x86/Conventions1.v
index ecfb85bf..646c4afb 100644
--- a/x86/Conventions1.v
+++ b/x86/Conventions1.v
@@ -299,7 +299,7 @@ Proof.
   assert (Y: forall ofs1 ofs2 p, forall_rpair (loc_argument_64_charact ofs2) p -> ofs1 <= ofs2 -> forall_rpair (loc_argument_64_charact ofs1) p).
   { destruct p; simpl; intuition eauto. }
   assert (Z: forall ofs, (2 | ofs) -> (2 | ofs + 2)).
-  { intros. apply Z.divide_add_r; auto. apply Zdivide_refl. }
+  { intros. apply Z.divide_add_r; auto. apply Z.divide_refl. }
 Opaque list_nth_z.
   induction tyl; simpl loc_arguments_64; intros.
   elim H.
@@ -339,10 +339,10 @@ Proof.
   assert (X: forall l, loc_argument_64_charact 0 l -> loc_argument_acceptable l).
   { unfold loc_argument_64_charact, loc_argument_acceptable.
     destruct l as [r | [] ofs ty]; auto.  intros [C|C]; auto.
-    intros [C D]. split; auto. apply Zdivide_trans with 2; auto.
+    intros [C D]. split; auto. apply Z.divide_trans with 2; auto.
     exists (2 / typealign ty); destruct ty; reflexivity.
   }
-  exploit loc_arguments_64_charact; eauto using Zdivide_0.
+  exploit loc_arguments_64_charact; eauto using Z.divide_0_r.
   unfold forall_rpair; destruct p; intuition auto.
 - (* 32 bits *)
   assert (X: forall l, loc_argument_32_charact 0 l -> loc_argument_acceptable l).
@@ -360,7 +360,7 @@ Remark size_arguments_32_above:
 Proof.
   induction tyl; simpl; intros.
   omega.
-  apply Zle_trans with (ofs0 + typesize a); auto.
+  apply Z.le_trans with (ofs0 + typesize a); auto.
   generalize (typesize_pos a); omega.
 Qed.
 
@@ -376,21 +376,21 @@ Proof.
     | None => size_arguments_64 tyl ir fr (ofs0 + 2)
     end).
   { destruct (list_nth_z int_param_regs ir); eauto.
-    apply Zle_trans with (ofs0 + 2); auto. omega. }
+    apply Z.le_trans with (ofs0 + 2); auto. omega. }
   assert (B: ofs0 <=
     match list_nth_z float_param_regs fr with
     | Some _ => size_arguments_64 tyl ir (fr + 1) ofs0
     | None => size_arguments_64 tyl ir fr (ofs0 + 2)
     end).
   { destruct (list_nth_z float_param_regs fr); eauto.
-    apply Zle_trans with (ofs0 + 2); auto. omega. }
+    apply Z.le_trans with (ofs0 + 2); auto. omega. }
   destruct a; auto.
 Qed.
 
 Lemma size_arguments_above:
   forall s, size_arguments s >= 0.
 Proof.
-  intros; unfold size_arguments. apply Zle_ge.
+  intros; unfold size_arguments. apply Z.le_ge.
   destruct Archi.ptr64; [apply size_arguments_64_above|apply size_arguments_32_above].
 Qed.
 
@@ -402,7 +402,7 @@ Proof.
   induction tyl as [ | t l]; simpl; intros x IN.
 - contradiction.
 - rewrite in_app_iff in IN; destruct IN as [IN|IN].
-+ apply Zle_trans with (x + typesize t); [|apply size_arguments_32_above].
++ apply Z.le_trans with (x + typesize t); [|apply size_arguments_32_above].
   Ltac decomp :=
   match goal with
   | [ H: _ \/ _ |- _ ] => destruct H; decomp
@@ -437,7 +437,7 @@ Proof.
   { intros. destruct (list_nth_z int_param_regs ir); simpl in H0; destruct H0.
   - discriminate.
   - eapply IHtyl; eauto.
-  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
+  - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
   - eapply IHtyl; eauto. }
   assert (B: forall ty0,
              In (S Outgoing ofs ty) (regs_of_rpairs
@@ -454,7 +454,7 @@ Proof.
   { intros. destruct (list_nth_z float_param_regs fr); simpl in H0; destruct H0.
   - discriminate.
   - eapply IHtyl; eauto.
-  - inv H0. apply Zle_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
+  - inv H0. apply Z.le_trans with (ofs + 2). specialize (T ty). omega. apply size_arguments_64_above.
   - eapply IHtyl; eauto. }
   destruct a; eauto.
 Qed.
diff --git a/x86/Op.v b/x86/Op.v
index 136c900b..02b04574 100644
--- a/x86/Op.v
+++ b/x86/Op.v
@@ -1311,7 +1311,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/x86/Stacklayout.v b/x86/Stacklayout.v
index 22c68099..d375febf 100644
--- a/x86/Stacklayout.v
+++ b/x86/Stacklayout.v
@@ -140,7 +140,7 @@ Proof.
   set (oretaddr := align (ostkdata + b.(bound_stack_data)) w).
   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.