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 /cfrontend/Cminorgenproof.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 'cfrontend/Cminorgenproof.v')
| -rw-r--r-- | cfrontend/Cminorgenproof.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v index a6d58f17..ffafc5d2 100644 --- a/cfrontend/Cminorgenproof.v +++ b/cfrontend/Cminorgenproof.v @@ -96,7 +96,7 @@ Proof. intros m1 FR1 FRL. transitivity (Mem.load chunk m1 b ofs). eapply IHfbl; eauto. intros. eapply H. eauto with coqlib. - eapply Mem.load_free; eauto. left. apply sym_not_equal. eapply H. auto with coqlib. + eapply Mem.load_free; eauto. left. apply not_eq_sym. eapply H. auto with coqlib. Qed. Lemma perm_freelist: @@ -775,7 +775,7 @@ Definition cenv_compat (cenv: compilenv) (vars: list (ident * Z)) (tsz: Z) : Pro PTree.get id cenv = Some ofs /\ Mem.inj_offset_aligned ofs sz /\ 0 <= ofs - /\ ofs + Zmax 0 sz <= tsz. + /\ ofs + Z.max 0 sz <= tsz. Definition cenv_separated (cenv: compilenv) (vars: list (ident * Z)) : Prop := forall id1 sz1 ofs1 id2 sz2 ofs2, @@ -901,7 +901,7 @@ Remark assign_variable_incr: Proof. simpl; intros. inv H. generalize (align_le stksz (block_alignment sz) (block_alignment_pos sz)). - assert (0 <= Zmax 0 sz). apply Zmax_bound_l. omega. + assert (0 <= Z.max 0 sz). apply Zmax_bound_l. omega. omega. Qed. @@ -914,7 +914,7 @@ Proof. Opaque assign_variable. destruct a as [id s]. simpl. intros. destruct (assign_variable (cenv, sz) (id, s)) as [cenv1 sz1] eqn:?. - apply Zle_trans with sz1. eapply assign_variable_incr; eauto. eauto. + apply Z.le_trans with sz1. eapply assign_variable_incr; eauto. eauto. Transparent assign_variable. Qed. @@ -925,8 +925,8 @@ Proof. intros; red; intros. apply Zdivides_trans with (block_alignment sz). unfold align_chunk. unfold block_alignment. - generalize Zone_divide; intro. - generalize Zdivide_refl; intro. + generalize Z.divide_1_l; intro. + generalize Z.divide_refl; intro. assert (2 | 4). exists 2; auto. assert (2 | 8). exists 4; auto. assert (4 | 8). exists 2; auto. @@ -942,10 +942,10 @@ Qed. Remark inj_offset_aligned_block': forall stacksize sz, - Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Zmax 0 sz). + Mem.inj_offset_aligned (align stacksize (block_alignment sz)) (Z.max 0 sz). Proof. intros. - replace (block_alignment sz) with (block_alignment (Zmax 0 sz)). + replace (block_alignment sz) with (block_alignment (Z.max 0 sz)). apply inj_offset_aligned_block. rewrite Zmax_spec. destruct (zlt sz 0); auto. transitivity 1. reflexivity. unfold block_alignment. rewrite zlt_true. auto. omega. |