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. --- powerpc/Conventions1.v | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) (limited to 'powerpc/Conventions1.v') 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. -- cgit