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 /powerpc/Conventions1.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 'powerpc/Conventions1.v')
| -rw-r--r-- | powerpc/Conventions1.v | 26 |
1 files changed, 13 insertions, 13 deletions
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. |