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 /common/Globalenvs.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 'common/Globalenvs.v')
| -rw-r--r-- | common/Globalenvs.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/common/Globalenvs.v b/common/Globalenvs.v index dd8a1eb9..72b48529 100644 --- a/common/Globalenvs.v +++ b/common/Globalenvs.v @@ -229,7 +229,7 @@ Program Definition add_global (ge: t) (idg: ident * globdef F V) : t := ge.(genv_public) (PTree.set idg#1 ge.(genv_next) ge.(genv_symb)) (PTree.set ge.(genv_next) idg#2 ge.(genv_defs)) - (Psucc ge.(genv_next)) + (Pos.succ ge.(genv_next)) _ _ _. Next Obligation. destruct ge; simpl in *. @@ -567,7 +567,7 @@ Proof. Qed. Definition advance_next (gl: list (ident * globdef F V)) (x: positive) := - List.fold_left (fun n g => Psucc n) gl x. + List.fold_left (fun n g => Pos.succ n) gl x. Remark genv_next_add_globals: forall gl ge, @@ -722,7 +722,7 @@ Qed. Remark alloc_global_nextblock: forall g m m', alloc_global m g = Some m' -> - Mem.nextblock m' = Psucc(Mem.nextblock m). + Mem.nextblock m' = Pos.succ(Mem.nextblock m). Proof. unfold alloc_global. intros. destruct g as [id [f|v]]. @@ -896,10 +896,10 @@ Lemma store_zeros_loadbytes: Proof. intros until n; functional induction (store_zeros m b p n); red; intros. - destruct n0. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. omegaContradiction. + rewrite Nat2Z.inj_succ in H1. omegaContradiction. - destruct (zeq p0 p). + subst p0. destruct n0. simpl. apply Mem.loadbytes_empty. omega. - rewrite inj_S in H1. rewrite inj_S. + rewrite Nat2Z.inj_succ in H1. rewrite Nat2Z.inj_succ. replace (Z.succ (Z.of_nat n0)) with (1 + Z.of_nat n0) by omega. change (list_repeat (S n0) (Byte Byte.zero)) with ((Byte Byte.zero :: nil) ++ list_repeat n0 (Byte Byte.zero)). @@ -1052,7 +1052,7 @@ Fixpoint load_store_init_data (m: mem) (b: block) (p: Z) (il: list init_data) {s /\ load_store_init_data m b (p + size_chunk Mptr) il' | Init_space n :: il' => read_as_zero m b p n - /\ load_store_init_data m b (p + Zmax n 0) il' + /\ load_store_init_data m b (p + Z.max n 0) il' end. Lemma store_init_data_list_charact: @@ -1425,7 +1425,7 @@ Remark advance_next_le: forall gl x, Ple x (advance_next gl x). Proof. induction gl; simpl; intros. apply Ple_refl. - apply Ple_trans with (Psucc x). apply Ple_succ. eauto. + apply Ple_trans with (Pos.succ x). apply Ple_succ. eauto. Qed. Lemma alloc_globals_neutral: @@ -1440,7 +1440,7 @@ Proof. exploit alloc_globals_nextblock; eauto. intros EQ. simpl in *. destruct (alloc_global ge m a) as [m1|] eqn:E; try discriminate. exploit alloc_global_neutral; eauto. - assert (Ple (Psucc (Mem.nextblock m)) (Mem.nextblock m')). + assert (Ple (Pos.succ (Mem.nextblock m)) (Mem.nextblock m')). { rewrite EQ. apply advance_next_le. } unfold Plt, Ple in *; zify; omega. Qed. |