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. --- cfrontend/Ctypes.v | 56 +++++++++++++++++++++++++++--------------------------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'cfrontend/Ctypes.v') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 8d6cdb24..036b768b 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -373,15 +373,15 @@ Lemma sizeof_alignof_compat: forall env t, naturally_aligned t -> (alignof env t | sizeof env t). Proof. induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. -- apply Zdivide_refl. -- destruct i; apply Zdivide_refl. +- apply Z.divide_refl. +- destruct i; apply Z.divide_refl. - exists (8 / Archi.align_int64). unfold Archi.align_int64; destruct Archi.ptr64; reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. -- apply Zdivide_refl. +- destruct f. apply Z.divide_refl. exists (8 / Archi.align_float64). unfold Archi.align_float64; destruct Archi.ptr64; reflexivity. +- apply Z.divide_refl. - apply Z.divide_mul_l; auto. -- apply Zdivide_refl. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- apply Z.divide_refl. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. +- destruct (env!i). apply co_sizeof_alignof. apply Z.divide_0_r. Qed. (** ** Size and alignment for composite definitions *) @@ -435,9 +435,9 @@ Lemma sizeof_struct_incr: Proof. induction m as [|[id t]]; simpl; intros. - omega. -- apply Zle_trans with (align cur (alignof env t)). +- apply Z.le_trans with (align cur (alignof env t)). apply align_le. apply alignof_pos. - apply Zle_trans with (align cur (alignof env t) + sizeof env t). + apply Z.le_trans with (align cur (alignof env t) + sizeof env t). generalize (sizeof_pos env t); omega. apply IHm. Qed. @@ -488,7 +488,7 @@ Proof. inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. exploit IHfld; eauto. intros [A B]. split; auto. - eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)). + eapply Z.le_trans; eauto. apply Z.le_trans with (align pos (alignof env t)). apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. Qed. @@ -627,7 +627,7 @@ Fixpoint alignof_blockcopy (env: composite_env) (t: type) : Z := Lemma alignof_blockcopy_1248: forall env ty, let a := alignof_blockcopy env ty in a = 1 \/ a = 2 \/ a = 4 \/ a = 8. Proof. - assert (X: forall co, let a := Zmin 8 (co_alignof co) in + assert (X: forall co, let a := Z.min 8 (co_alignof co) in a = 1 \/ a = 2 \/ a = 4 \/ a = 8). { intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. @@ -635,7 +635,7 @@ Proof. destruct n; auto. destruct n; auto. right; right; right. apply Z.min_l. - rewrite two_power_nat_two_p. rewrite ! inj_S. + rewrite two_power_nat_two_p. rewrite ! Nat2Z.inj_succ. change 8 with (two_p 3). apply two_p_monotone. omega. } induction ty; simpl. @@ -661,28 +661,28 @@ Lemma sizeof_alignof_blockcopy_compat: Proof. assert (X: forall co, (Z.min 8 (co_alignof co) | co_sizeof co)). { - intros. apply Zdivide_trans with (co_alignof co). 2: apply co_sizeof_alignof. + intros. apply Z.divide_trans with (co_alignof co). 2: apply co_sizeof_alignof. destruct (co_alignof_two_p co) as [n EQ]. rewrite EQ. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. - destruct n. apply Zdivide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. + destruct n. apply Z.divide_refl. apply Z.min_case. exists (two_p (Z.of_nat n)). change 8 with (two_p 3). rewrite <- two_p_is_exp by omega. - rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. - apply Zdivide_refl. + rewrite two_power_nat_two_p. rewrite !Nat2Z.inj_succ. f_equal. omega. + apply Z.divide_refl. } induction ty; simpl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. - apply Zdivide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. + apply Z.divide_refl. apply Z.divide_mul_l. auto. - apply Zdivide_refl. - destruct (env!i). apply X. apply Zdivide_0. - destruct (env!i). apply X. apply Zdivide_0. + apply Z.divide_refl. + destruct (env!i). apply X. apply Z.divide_0_r. + destruct (env!i). apply X. apply Z.divide_0_r. Qed. (** Type ranks *) @@ -707,7 +707,7 @@ Fixpoint rank_type (ce: composite_env) (t: type) : nat := Fixpoint rank_members (ce: composite_env) (m: members) : nat := match m with | nil => 0%nat - | (id, t) :: m => Peano.max (rank_type ce t) (rank_members ce m) + | (id, t) :: m => Init.Nat.max (rank_type ce t) (rank_members ce m) end. (** ** C types and back-end types *) @@ -818,7 +818,7 @@ Program Definition composite_of_def co_sizeof_alignof := _ |} end. Next Obligation. - apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. + apply Z.le_ge. eapply Z.le_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. Defined. Next Obligation. -- cgit