Remove coq warnings (#28)

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

5 files changed, 23 insertions, 23 deletions

diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v
index bf75d2e0..9f258e3d 100644
--- a/powerpc/Asmgenproof.v
+++ b/powerpc/Asmgenproof.v
@@ -854,7 +854,7 @@ Local Transparent destroyed_by_jumptable.
   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/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v
index e5736277..460fa670 100644
--- a/powerpc/Asmgenproof1.v
+++ b/powerpc/Asmgenproof1.v
@@ -39,9 +39,9 @@ Proof.
   intros. unfold high_u, low_u.
   rewrite Int.shl_rolm. rewrite Int.shru_rolm.
   rewrite Int.rolm_rolm.
-  change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
+  change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16))
                             (Int.repr 16))
-                   (Int.repr (Z_of_nat Int.wordsize)))
+                   (Int.repr (Z.of_nat Int.wordsize)))
     with (Int.zero).
   rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib.
   exact (Int.and_mone n).
@@ -54,9 +54,9 @@ Proof.
   intros. unfold high_u, low_u.
   rewrite Int.shl_rolm. rewrite Int.shru_rolm.
   rewrite Int.rolm_rolm.
-  change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat Int.wordsize)) (Int.repr 16))
+  change (Int.modu (Int.add (Int.sub (Int.repr (Z.of_nat Int.wordsize)) (Int.repr 16))
                             (Int.repr 16))
-                   (Int.repr (Z_of_nat Int.wordsize)))
+                   (Int.repr (Z.of_nat Int.wordsize)))
     with (Int.zero).
   rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib.
   exact (Int.and_mone n).
@@ -198,7 +198,7 @@ Hint Resolve ireg_of_not_GPR0': asmgen.
 Lemma preg_of_not_LR:
   forall r, LR <> preg_of r.
 Proof.
-  intros. auto using sym_not_equal with asmgen.
+  intros. auto using not_eq_sym with asmgen.
 Qed.
 
 Lemma preg_notin_LR:
@@ -1243,7 +1243,7 @@ Opaque Val.add.
   econstructor; split. eapply exec_straight_trans.
   eapply exec_straight_two; simpl; reflexivity.
   eapply exec_straight_two; simpl; reflexivity.
-  split. assert (GPR0 <> x0) by (apply sym_not_equal; eauto with asmgen).
+  split. assert (GPR0 <> x0) by (apply not_eq_sym; eauto with asmgen).
   Simpl. rewrite ! gpr_or_zero_zero. rewrite ! gpr_or_zero_not_zero by eauto with asmgen. Simpl.
   rewrite low_high_half_zero. auto.
   intros; Simpl.
diff --git a/powerpc/Conventions1.v b/powerpc/Conventions1.v
index 2793fbfb..1de55c1a 100644
--- a/powerpc/Conventions1.v
+++ b/powerpc/Conventions1.v
@@ -370,30 +370,30 @@ Proof.
   induction tyl; simpl; intros.
   omega.
   destruct a.
-  destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega.
+  destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
   destruct (list_nth_z float_param_regs fr); eauto.
-  apply Zle_trans with (align ofs0 2). apply align_le; omega.
-  apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
   set (ir' := align ir 2).
   destruct (list_nth_z int_param_regs ir'); eauto.
   destruct (list_nth_z int_param_regs (ir' + 1)); eauto.
-  apply Zle_trans with (align ofs0 2). apply align_le; omega.
-  apply Zle_trans with (align ofs0 2 + 2); auto; omega.
-  apply Zle_trans with (align ofs0 2). apply align_le; omega.
-  apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
+  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
   destruct (list_nth_z float_param_regs fr); eauto.
-  apply Zle_trans with (align ofs0 2). apply align_le; omega.
-  apply Zle_trans with (align ofs0 2 + 2); auto; omega.
-  destruct (list_nth_z int_param_regs ir); eauto. apply Zle_trans with (ofs0 + 1); auto; omega.
+  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
+  destruct (list_nth_z int_param_regs ir); eauto. apply Z.le_trans with (ofs0 + 1); auto; omega.
   destruct (list_nth_z float_param_regs fr); eauto.
-  apply Zle_trans with (align ofs0 2). apply align_le; omega.
-  apply Zle_trans with (align ofs0 2 + 2); auto; omega.
+  apply Z.le_trans with (align ofs0 2). apply align_le; omega.
+  apply Z.le_trans with (align ofs0 2 + 2); auto; omega.
 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.
   apply size_arguments_rec_above.
 Qed.
 
diff --git a/powerpc/Op.v b/powerpc/Op.v
index 263c1bd8..e6f942c1 100644
--- a/powerpc/Op.v
+++ b/powerpc/Op.v
@@ -1042,7 +1042,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/powerpc/Stacklayout.v b/powerpc/Stacklayout.v
index 17104b33..cb3806bd 100644
--- a/powerpc/Stacklayout.v
+++ b/powerpc/Stacklayout.v
@@ -138,8 +138,8 @@ Proof.
   split. exists (fe_ofs_arg / 8); reflexivity.
   split. apply align_divides; omega.
   split. apply align_divides; omega.
-  split. apply Zdivide_0.
+  split. apply Z.divide_0_r.
   apply Z.divide_add_r.
-    apply Zdivide_trans with 8. exists 2; auto. apply align_divides; omega.
+    apply Z.divide_trans with 8. exists 2; auto. apply align_divides; omega.
     apply Z.divide_factor_l.
 Qed.