From 8d5c6bb8f0cac1339dec7b730997ee30b1517073 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bschommer@users.noreply.github.com>
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.
---
 common/AST.v        |   2 +-
 common/Behaviors.v  |   2 +-
 common/Events.v     |   8 +--
 common/Globalenvs.v |  16 +++---
 common/Memdata.v    |  50 +++++++++---------
 common/Memory.v     | 146 ++++++++++++++++++++++++++--------------------------
 common/Memtype.v    |  20 +++----
 common/Separation.v |   8 +--
 common/Switch.v     |  10 ++--
 9 files changed, 131 insertions(+), 131 deletions(-)

(limited to 'common')

diff --git a/common/AST.v b/common/AST.v
index 9eeca5b1..a072ef29 100644
--- a/common/AST.v
+++ b/common/AST.v
@@ -214,7 +214,7 @@ Definition init_data_size (i: init_data) : Z :=
   | Init_float32 _ => 4
   | Init_float64 _ => 8
   | Init_addrof _ _ => if Archi.ptr64 then 8 else 4
-  | Init_space n => Zmax n 0
+  | Init_space n => Z.max n 0
   end.
 
 Fixpoint init_data_list_size (il: list init_data) {struct il} : Z :=
diff --git a/common/Behaviors.v b/common/Behaviors.v
index ef99b205..92bd708f 100644
--- a/common/Behaviors.v
+++ b/common/Behaviors.v
@@ -187,7 +187,7 @@ CoFixpoint build_traceinf' (s1: state L) (t1: trace) (ST: Star L s0 t1 s1) : tra
   match reacts' ST with
   | existT s2 (exist t2 (conj A B)) =>
       Econsinf' t2
-                (build_traceinf' (star_trans ST A (refl_equal _)))
+                (build_traceinf' (star_trans ST A (eq_refl _)))
                 B
   end.
 
diff --git a/common/Events.v b/common/Events.v
index ab804aa7..63922bc5 100644
--- a/common/Events.v
+++ b/common/Events.v
@@ -999,7 +999,7 @@ Proof.
   assert (SZ: v2 = Vptrofs sz).
   { unfold Vptrofs in *. destruct Archi.ptr64; inv H5; auto. }
   subst v2.
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. apply Zle_refl.
+  exploit Mem.alloc_extends; eauto. apply Z.le_refl. apply Z.le_refl.
   intros [m3' [A B]].
   exploit Mem.store_within_extends. eexact B. eauto. eauto.
   intros [m2' [C D]].
@@ -1011,11 +1011,11 @@ Proof.
   assert (SZ: v' = Vptrofs sz).
   { unfold Vptrofs in *. destruct Archi.ptr64; inv H6; auto. }
   subst v'.
-  exploit Mem.alloc_parallel_inject; eauto. apply Zle_refl. apply Zle_refl.
+  exploit Mem.alloc_parallel_inject; eauto. apply Z.le_refl. apply Z.le_refl.
   intros [f' [m3' [b' [ALLOC [A [B [C D]]]]]]].
   exploit Mem.store_mapped_inject. eexact A. eauto. eauto.
   instantiate (1 := Vptrofs sz). unfold Vptrofs; destruct Archi.ptr64; constructor.
-  rewrite Zplus_0_r. intros [m2' [E G]].
+  rewrite Z.add_0_r. intros [m2' [E G]].
   exists f'; exists (Vptr b' Ptrofs.zero); exists m2'; intuition auto.
   econstructor; eauto.
   econstructor. eauto. auto.
@@ -1206,7 +1206,7 @@ Proof.
   assert (RPSRC: Mem.range_perm m1 bsrc (Ptrofs.unsigned osrc) (Ptrofs.unsigned osrc + sz) Cur Nonempty).
     eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem.
   assert (RPDST: Mem.range_perm m1 bdst (Ptrofs.unsigned odst) (Ptrofs.unsigned odst + sz) Cur Nonempty).
-    replace sz with (Z_of_nat (length bytes)).
+    replace sz with (Z.of_nat (length bytes)).
     eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem.
     rewrite LEN. apply nat_of_Z_eq. omega.
   assert (PSRC: Mem.perm m1 bsrc (Ptrofs.unsigned osrc) Cur Nonempty).
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.
diff --git a/common/Memdata.v b/common/Memdata.v
index 0aed4644..a9ed48b4 100644
--- a/common/Memdata.v
+++ b/common/Memdata.v
@@ -53,7 +53,7 @@ Definition size_chunk_nat (chunk: memory_chunk) : nat :=
   nat_of_Z(size_chunk chunk).
 
 Lemma size_chunk_conv:
-  forall chunk, size_chunk chunk = Z_of_nat (size_chunk_nat chunk).
+  forall chunk, size_chunk chunk = Z.of_nat (size_chunk_nat chunk).
 Proof.
   intros. destruct chunk; reflexivity.
 Qed.
@@ -111,7 +111,7 @@ Qed.
 Lemma align_size_chunk_divides:
   forall chunk, (align_chunk chunk | size_chunk chunk).
 Proof.
-  intros. destruct chunk; simpl; try apply Zdivide_refl; exists 2; auto.
+  intros. destruct chunk; simpl; try apply Z.divide_refl; exists 2; auto.
 Qed.
 
 Lemma align_le_divides:
@@ -120,7 +120,7 @@ Lemma align_le_divides:
 Proof.
   intros. destruct chunk1; destruct chunk2; simpl in *;
   solve [ omegaContradiction
-        | apply Zdivide_refl
+        | apply Z.divide_refl
         | exists 2; reflexivity
         | exists 4; reflexivity
         | exists 8; reflexivity ].
@@ -209,15 +209,15 @@ Qed.
 
 Lemma int_of_bytes_of_int:
   forall n x,
-  int_of_bytes (bytes_of_int n x) = x mod (two_p (Z_of_nat n * 8)).
+  int_of_bytes (bytes_of_int n x) = x mod (two_p (Z.of_nat n * 8)).
 Proof.
   induction n; intros.
   simpl. rewrite Zmod_1_r. auto.
 Opaque Byte.wordsize.
-  rewrite inj_S. simpl.
-  replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega.
+  rewrite Nat2Z.inj_succ. simpl.
+  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega.
   rewrite two_p_is_exp; try omega.
-  rewrite Zmod_recombine. rewrite IHn. rewrite Zplus_comm.
+  rewrite Zmod_recombine. rewrite IHn. rewrite Z.add_comm.
   change (Byte.unsigned (Byte.repr x)) with (Byte.Z_mod_modulus x).
   rewrite Byte.Z_mod_modulus_eq. reflexivity.
   apply two_p_gt_ZERO. omega. apply two_p_gt_ZERO. omega.
@@ -232,7 +232,7 @@ Proof.
 Qed.
 
 Lemma decode_encode_int:
-  forall n x, decode_int (encode_int n x) = x mod (two_p (Z_of_nat n * 8)).
+  forall n x, decode_int (encode_int n x) = x mod (two_p (Z.of_nat n * 8)).
 Proof.
   unfold decode_int, encode_int; intros. rewrite rev_if_be_involutive.
   apply int_of_bytes_of_int.
@@ -272,19 +272,19 @@ Qed.
 
 Lemma bytes_of_int_mod:
   forall n x y,
-  Int.eqmod (two_p (Z_of_nat n * 8)) x y ->
+  Int.eqmod (two_p (Z.of_nat n * 8)) x y ->
   bytes_of_int n x = bytes_of_int n y.
 Proof.
   induction n.
   intros; simpl; auto.
   intros until y.
-  rewrite inj_S.
-  replace (Zsucc (Z_of_nat n) * 8) with (Z_of_nat n * 8 + 8) by omega.
+  rewrite Nat2Z.inj_succ.
+  replace (Z.succ (Z.of_nat n) * 8) with (Z.of_nat n * 8 + 8) by omega.
   rewrite two_p_is_exp; try omega.
   intro EQM.
   simpl; decEq.
   apply Byte.eqm_samerepr. red.
-  eapply Int.eqmod_divides; eauto. apply Zdivide_factor_l.
+  eapply Int.eqmod_divides; eauto. apply Z.divide_factor_r.
   apply IHn.
   destruct EQM as [k EQ]. exists k. rewrite EQ.
   rewrite <- Z_div_plus_full_l. decEq. change (two_p 8) with 256. ring. omega.
@@ -354,7 +354,7 @@ Fixpoint check_value (n: nat) (v: val) (q: quantity) (vl: list memval)
   match n, vl with
   | O, nil => true
   | S m, Fragment v' q' m' :: vl' =>
-      Val.eq v v' && quantity_eq q q' && beq_nat m m' && check_value m v q vl'
+      Val.eq v v' && quantity_eq q q' && Nat.eqb m m' && check_value m v q vl'
   | _, _ => false
   end.
 
@@ -728,7 +728,7 @@ Proof.
     destruct (size_quantity_nat_pos q) as [sz EQ]. rewrite EQ.
     simpl. unfold proj_sumbool. rewrite dec_eq_true.
     destruct (quantity_eq q q0); auto.
-    destruct (beq_nat sz n) eqn:EQN; auto.
+    destruct (Nat.eqb sz n) eqn:EQN; auto.
     destruct (check_value sz v q mvl) eqn:CHECK; auto.
     simpl. apply beq_nat_true in EQN. subst n q0. constructor. auto.
     destruct H0 as [E|[E|[E|E]]]; subst chunk; destruct q; auto || discriminate.
@@ -943,22 +943,22 @@ Qed.
 
 Lemma int_of_bytes_append:
   forall l2 l1,
-  int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z_of_nat (length l1) * 8).
+  int_of_bytes (l1 ++ l2) = int_of_bytes l1 + int_of_bytes l2 * two_p (Z.of_nat (length l1) * 8).
 Proof.
   induction l1; simpl int_of_bytes; intros.
   simpl. ring.
-  simpl length. rewrite inj_S.
-  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z_of_nat (length l1) * 8 + 8) by omega.
+  simpl length. rewrite Nat2Z.inj_succ.
+  replace (Z.succ (Z.of_nat (length l1)) * 8) with (Z.of_nat (length l1) * 8 + 8) by omega.
   rewrite two_p_is_exp. change (two_p 8) with 256. rewrite IHl1. ring.
   omega. omega.
 Qed.
 
 Lemma int_of_bytes_range:
-  forall l, 0 <= int_of_bytes l < two_p (Z_of_nat (length l) * 8).
+  forall l, 0 <= int_of_bytes l < two_p (Z.of_nat (length l) * 8).
 Proof.
   induction l; intros.
   simpl. omega.
-  simpl length. rewrite inj_S.
+  simpl length. rewrite Nat2Z.inj_succ.
   replace (Z.succ (Z.of_nat (length l)) * 8) with (Z.of_nat (length l) * 8 + 8) by omega.
   rewrite two_p_is_exp. change (two_p 8) with 256.
   simpl int_of_bytes. generalize (Byte.unsigned_range a).
@@ -1024,21 +1024,21 @@ Qed.
 
 Lemma bytes_of_int_append:
   forall n2 x2 n1 x1,
-  0 <= x1 < two_p (Z_of_nat n1 * 8) ->
-  bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z_of_nat n1 * 8)) =
+  0 <= x1 < two_p (Z.of_nat n1 * 8) ->
+  bytes_of_int (n1 + n2) (x1 + x2 * two_p (Z.of_nat n1 * 8)) =
   bytes_of_int n1 x1 ++ bytes_of_int n2 x2.
 Proof.
   induction n1; intros.
 - simpl in *. f_equal. omega.
 - assert (E: two_p (Z.of_nat (S n1) * 8) = two_p (Z.of_nat n1 * 8) * 256).
   {
-    rewrite inj_S. change 256 with (two_p 8). rewrite <- two_p_is_exp.
+    rewrite Nat2Z.inj_succ. change 256 with (two_p 8). rewrite <- two_p_is_exp.
     f_equal. omega. omega. omega.
   }
   rewrite E in *. simpl. f_equal.
   apply Byte.eqm_samerepr. exists (x2 * two_p (Z.of_nat n1 * 8)).
   change Byte.modulus with 256. ring.
-  rewrite Zmult_assoc. rewrite Z_div_plus. apply IHn1.
+  rewrite Z.mul_assoc. rewrite Z_div_plus. apply IHn1.
   apply Zdiv_interval_1. omega. apply two_p_gt_ZERO; omega. omega.
   assumption. omega.
 Qed.
@@ -1051,8 +1051,8 @@ Proof.
   intros. transitivity (bytes_of_int (4 + 4) (Int64.unsigned (Int64.ofwords (Int64.hiword i) (Int64.loword i)))).
   f_equal. f_equal. rewrite Int64.ofwords_recompose. auto.
   rewrite Int64.ofwords_add'.
-  change 32 with (Z_of_nat 4 * 8).
-  rewrite Zplus_comm. apply bytes_of_int_append. apply Int.unsigned_range.
+  change 32 with (Z.of_nat 4 * 8).
+  rewrite Z.add_comm. apply bytes_of_int_append. apply Int.unsigned_range.
 Qed.
 
 Lemma encode_val_int64:
diff --git a/common/Memory.v b/common/Memory.v
index 8bb69c02..2cf1c3ab 100644
--- a/common/Memory.v
+++ b/common/Memory.v
@@ -275,7 +275,7 @@ Lemma valid_access_compat:
   valid_access m chunk2 b ofs p.
 Proof.
   intros. inv H1. rewrite H in H2. constructor; auto.
-  eapply Zdivide_trans; eauto. eapply align_le_divides; eauto.
+  eapply Z.divide_trans; eauto. eapply align_le_divides; eauto.
 Qed.
 
 Lemma valid_access_dec:
@@ -311,7 +311,7 @@ Proof.
   intros. rewrite valid_pointer_nonempty_perm.
   split; intros.
   split. simpl; red; intros. replace ofs0 with ofs by omega. auto.
-  simpl. apply Zone_divide.
+  simpl. apply Z.divide_1_l.
   destruct H. apply H. simpl. omega.
 Qed.
 
@@ -367,7 +367,7 @@ Program Definition alloc (m: mem) (lo hi: Z) :=
          (PMap.set m.(nextblock)
                    (fun ofs k => if zle lo ofs && zlt ofs hi then Some Freeable else None)
                    m.(mem_access))
-         (Psucc m.(nextblock))
+         (Pos.succ m.(nextblock))
          _ _ _,
    m.(nextblock)).
 Next Obligation.
@@ -475,12 +475,12 @@ Fixpoint setN (vl: list memval) (p: Z) (c: ZMap.t memval) {struct vl}: ZMap.t me
 
 Remark setN_other:
   forall vl c p q,
-  (forall r, p <= r < p + Z_of_nat (length vl) -> r <> q) ->
+  (forall r, p <= r < p + Z.of_nat (length vl) -> r <> q) ->
   ZMap.get q (setN vl p c) = ZMap.get q c.
 Proof.
   induction vl; intros; simpl.
   auto.
-  simpl length in H. rewrite inj_S in H.
+  simpl length in H. rewrite Nat2Z.inj_succ in H.
   transitivity (ZMap.get q (ZMap.set p a c)).
   apply IHvl. intros. apply H. omega.
   apply ZMap.gso. apply not_eq_sym. apply H. omega.
@@ -488,7 +488,7 @@ Qed.
 
 Remark setN_outside:
   forall vl c p q,
-  q < p \/ q >= p + Z_of_nat (length vl) ->
+  q < p \/ q >= p + Z.of_nat (length vl) ->
   ZMap.get q (setN vl p c) = ZMap.get q c.
 Proof.
   intros. apply setN_other.
@@ -508,16 +508,16 @@ Qed.
 
 Remark getN_exten:
   forall c1 c2 n p,
-  (forall i, p <= i < p + Z_of_nat n -> ZMap.get i c1 = ZMap.get i c2) ->
+  (forall i, p <= i < p + Z.of_nat n -> ZMap.get i c1 = ZMap.get i c2) ->
   getN n p c1 = getN n p c2.
 Proof.
-  induction n; intros. auto. rewrite inj_S in H. simpl. decEq.
+  induction n; intros. auto. rewrite Nat2Z.inj_succ in H. simpl. decEq.
   apply H. omega. apply IHn. intros. apply H. omega.
 Qed.
 
 Remark getN_setN_disjoint:
   forall vl q c n p,
-  Intv.disjoint (p, p + Z_of_nat n) (q, q + Z_of_nat (length vl)) ->
+  Intv.disjoint (p, p + Z.of_nat n) (q, q + Z.of_nat (length vl)) ->
   getN n p (setN vl q c) = getN n p c.
 Proof.
   intros. apply getN_exten. intros. apply setN_other.
@@ -526,7 +526,7 @@ Qed.
 
 Remark getN_setN_outside:
   forall vl q c n p,
-  p + Z_of_nat n <= q \/ q + Z_of_nat (length vl) <= p ->
+  p + Z.of_nat n <= q \/ q + Z.of_nat (length vl) <= p ->
   getN n p (setN vl q c) = getN n p c.
 Proof.
   intros. apply getN_setN_disjoint. apply Intv.disjoint_range. auto.
@@ -575,7 +575,7 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem :=
   or [None] if the accessed locations are not writable. *)
 
 Program Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem :=
-  if range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Cur Writable then
+  if range_perm_dec m b ofs (ofs + Z.of_nat (length bytes)) Cur Writable then
     Some (mkmem
              (PMap.set b (setN bytes ofs (m.(mem_contents)#b)) m.(mem_contents))
              m.(mem_access)
@@ -797,12 +797,12 @@ Qed.
 
 Lemma getN_concat:
   forall c n1 n2 p,
-  getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z_of_nat n1) c.
+  getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z.of_nat n1) c.
 Proof.
   induction n1; intros.
   simpl. decEq. omega.
-  rewrite inj_S. simpl. decEq.
-  replace (p + Zsucc (Z_of_nat n1)) with ((p + 1) + Z_of_nat n1) by omega.
+  rewrite Nat2Z.inj_succ. simpl. decEq.
+  replace (p + Z.succ (Z.of_nat n1)) with ((p + 1) + Z.of_nat n1) by omega.
   auto.
 Qed.
 
@@ -861,14 +861,14 @@ Proof.
   remember (size_chunk_nat ch) as n; clear Heqn.
   revert ofs H; induction n; intros; simpl; auto.
   f_equal.
-  rewrite inj_S in H.
+  rewrite Nat2Z.inj_succ in H.
   replace ofs with (ofs+0) by omega.
   apply H; omega.
   apply IHn.
   intros.
-  rewrite <- Zplus_assoc.
+  rewrite <- Z.add_assoc.
   apply H.
-  rewrite inj_S. omega.
+  rewrite Nat2Z.inj_succ. omega.
 Qed.
 
 Theorem load_int64_split:
@@ -891,7 +891,7 @@ Proof.
   intros L1.
   change 4 with (size_chunk Mint32) in LB2.
   exploit loadbytes_load. eexact LB2.
-  simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
   intros L2.
   exists (decode_val Mint32 (if Archi.big_endian then bytes1 else bytes2));
   exists (decode_val Mint32 (if Archi.big_endian then bytes2 else bytes1)).
@@ -1059,7 +1059,7 @@ Proof.
   replace (size_chunk_nat chunk') with (length (encode_val chunk v)).
   rewrite getN_setN_same. apply decode_encode_val_general.
   rewrite encode_val_length. repeat rewrite size_chunk_conv in H.
-  apply inj_eq_rev; auto.
+  apply Nat2Z.inj; auto.
 Qed.
 
 Theorem load_store_similar_2:
@@ -1139,12 +1139,12 @@ Qed.
 
 Lemma setN_in:
   forall vl p q c,
-  p <= q < p + Z_of_nat (length vl) ->
+  p <= q < p + Z.of_nat (length vl) ->
   In (ZMap.get q (setN vl p c)) vl.
 Proof.
   induction vl; intros.
   simpl in H. omegaContradiction.
-  simpl length in H. rewrite inj_S in H. simpl.
+  simpl length in H. rewrite Nat2Z.inj_succ in H. simpl.
   destruct (zeq p q). subst q. rewrite setN_outside. rewrite ZMap.gss.
   auto with coqlib. omega.
   right. apply IHvl. omega.
@@ -1152,12 +1152,12 @@ Qed.
 
 Lemma getN_in:
   forall c q n p,
-  p <= q < p + Z_of_nat n ->
+  p <= q < p + Z.of_nat n ->
   In (ZMap.get q c) (getN n p c).
 Proof.
   induction n; intros.
   simpl in H; omegaContradiction.
-  rewrite inj_S in H. simpl. destruct (zeq p q).
+  rewrite Nat2Z.inj_succ in H. simpl. destruct (zeq p q).
   subst q. auto.
   right. apply IHn. omega.
 Qed.
@@ -1206,7 +1206,7 @@ Proof.
 + left; split. omega. unfold c'. simpl. apply setN_in.
   assert (Z.of_nat (length (mv1 :: mvl)) = size_chunk chunk).
   { rewrite <- ENC; rewrite encode_val_length. rewrite size_chunk_conv; auto. }
-  simpl length in H3. rewrite inj_S in H3. omega.
+  simpl length in H3. rewrite Nat2Z.inj_succ in H3. omega.
 (* If ofs > ofs':  the load reads (at ofs) the first byte from the write.
        ofs'   ofs   ofs'+|chunk'|
                [-------------------]  write
@@ -1214,8 +1214,8 @@ Proof.
 *)
 + right; split. omega. replace mv1 with (ZMap.get ofs c').
   apply getN_in.
-  assert (size_chunk chunk' = Zsucc (Z.of_nat sz')).
-  { rewrite size_chunk_conv. rewrite SIZE'. rewrite inj_S; auto. }
+  assert (size_chunk chunk' = Z.succ (Z.of_nat sz')).
+  { rewrite size_chunk_conv. rewrite SIZE'. rewrite Nat2Z.inj_succ; auto. }
   omega.
   unfold c'. simpl. rewrite setN_outside by omega. apply ZMap.gss.
 Qed.
@@ -1391,11 +1391,11 @@ Qed.
 
 Theorem range_perm_storebytes:
   forall m1 b ofs bytes,
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
+  range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable ->
   { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
 Proof.
   intros. unfold storebytes.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable).
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable).
   econstructor; reflexivity.
   contradiction.
 Defined.
@@ -1407,7 +1407,7 @@ Theorem storebytes_store:
   store chunk m1 b ofs v = Some m2.
 Proof.
   unfold storebytes, store. intros.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable); inv H.
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length (encode_val chunk v))) Cur Writable); inv H.
   destruct (valid_access_dec m1 chunk b ofs Writable).
   f_equal. apply mkmem_ext; auto.
   elim n. constructor; auto.
@@ -1421,7 +1421,7 @@ Theorem store_storebytes:
 Proof.
   unfold storebytes, store. intros.
   destruct (valid_access_dec m1 chunk b ofs Writable); inv H.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Cur Writable).
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length (encode_val chunk v))) Cur Writable).
   f_equal. apply mkmem_ext; auto.
   destruct v0.  elim n.
   rewrite encode_val_length. rewrite <- size_chunk_conv. auto.
@@ -1438,7 +1438,7 @@ Hypothesis STORE: storebytes m1 b ofs bytes = Some m2.
 Lemma storebytes_access: mem_access m2 = mem_access m1.
 Proof.
   unfold storebytes in STORE.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
@@ -1447,7 +1447,7 @@ Lemma storebytes_mem_contents:
    mem_contents m2 = PMap.set b (setN bytes ofs m1.(mem_contents)#b) m1.(mem_contents).
 Proof.
   unfold storebytes in STORE.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
@@ -1487,7 +1487,7 @@ Theorem nextblock_storebytes:
 Proof.
   intros.
   unfold storebytes in STORE.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
@@ -1507,20 +1507,20 @@ Qed.
 Local Hint Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem.
 
 Theorem storebytes_range_perm:
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable.
+  range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable.
 Proof.
   intros.
   unfold storebytes in STORE.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   inv STORE.
   auto.
 Qed.
 
 Theorem loadbytes_storebytes_same:
-  loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
+  loadbytes m2 b ofs (Z.of_nat (length bytes)) = Some bytes.
 Proof.
   intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes.
-  destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable);
+  destruct (range_perm_dec m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable);
   try discriminate.
   rewrite pred_dec_true.
   decEq. inv STORE2; simpl. rewrite PMap.gss. rewrite nat_of_Z_of_nat.
@@ -1531,7 +1531,7 @@ Qed.
 Theorem loadbytes_storebytes_disjoint:
   forall b' ofs' len,
   len >= 0 ->
-  b' <> b \/ Intv.disjoint (ofs', ofs' + len) (ofs, ofs + Z_of_nat (length bytes)) ->
+  b' <> b \/ Intv.disjoint (ofs', ofs' + len) (ofs, ofs + Z.of_nat (length bytes)) ->
   loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.
 Proof.
   intros. unfold loadbytes.
@@ -1551,7 +1551,7 @@ Theorem loadbytes_storebytes_other:
   len >= 0 ->
   b' <> b
   \/ ofs' + len <= ofs
-  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  \/ ofs + Z.of_nat (length bytes) <= ofs' ->
   loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.
 Proof.
   intros. apply loadbytes_storebytes_disjoint; auto.
@@ -1562,7 +1562,7 @@ Theorem load_storebytes_other:
   forall chunk b' ofs',
   b' <> b
   \/ ofs' + size_chunk chunk <= ofs
-  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  \/ ofs + Z.of_nat (length bytes) <= ofs' ->
   load chunk m2 b' ofs' = load chunk m1 b' ofs'.
 Proof.
   intros. unfold load.
@@ -1581,29 +1581,29 @@ End STOREBYTES.
 
 Lemma setN_concat:
   forall bytes1 bytes2 ofs c,
-  setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z_of_nat (length bytes1)) (setN bytes1 ofs c).
+  setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z.of_nat (length bytes1)) (setN bytes1 ofs c).
 Proof.
   induction bytes1; intros.
   simpl. decEq. omega.
-  simpl length. rewrite inj_S. simpl. rewrite IHbytes1. decEq. omega.
+  simpl length. rewrite Nat2Z.inj_succ. simpl. rewrite IHbytes1. decEq. omega.
 Qed.
 
 Theorem storebytes_concat:
   forall m b ofs bytes1 m1 bytes2 m2,
   storebytes m b ofs bytes1 = Some m1 ->
-  storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 ->
+  storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2 ->
   storebytes m b ofs (bytes1 ++ bytes2) = Some m2.
 Proof.
   intros. generalize H; intro ST1. generalize H0; intro ST2.
   unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2.
-  destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Cur Writable); try congruence.
-  destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Cur Writable); try congruence.
-  destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Cur Writable).
+  destruct (range_perm_dec m b ofs (ofs + Z.of_nat(length bytes1)) Cur Writable); try congruence.
+  destruct (range_perm_dec m1 b (ofs + Z.of_nat(length bytes1)) (ofs + Z.of_nat(length bytes1) + Z.of_nat(length bytes2)) Cur Writable); try congruence.
+  destruct (range_perm_dec m b ofs (ofs + Z.of_nat (length (bytes1 ++ bytes2))) Cur Writable).
   inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto.
   rewrite PMap.gss.  rewrite setN_concat. symmetry. apply PMap.set2.
   elim n.
-  rewrite app_length. rewrite inj_plus. red; intros.
-  destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))).
+  rewrite app_length. rewrite Nat2Z.inj_add. red; intros.
+  destruct (zlt ofs0 (ofs + Z.of_nat(length bytes1))).
   apply r. omega.
   eapply perm_storebytes_2; eauto. apply r0. omega.
 Qed.
@@ -1613,15 +1613,15 @@ Theorem storebytes_split:
   storebytes m b ofs (bytes1 ++ bytes2) = Some m2 ->
   exists m1,
      storebytes m b ofs bytes1 = Some m1
-  /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2.
+  /\ storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2.
 Proof.
   intros.
   destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1].
   red; intros. exploit storebytes_range_perm; eauto. rewrite app_length.
-  rewrite inj_plus. omega.
-  destruct (range_perm_storebytes m1 b (ofs + Z_of_nat (length bytes1)) bytes2) as [m2' ST2].
+  rewrite Nat2Z.inj_add. omega.
+  destruct (range_perm_storebytes m1 b (ofs + Z.of_nat (length bytes1)) bytes2) as [m2' ST2].
   red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm.
-  eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite inj_plus. omega.
+  eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite Nat2Z.inj_add. omega.
   auto.
   assert (Some m2 = Some m2').
   rewrite <- H. eapply storebytes_concat; eauto.
@@ -1646,7 +1646,7 @@ Proof.
   apply storebytes_store. exact SB1.
   simpl. apply Zdivides_trans with 8; auto. exists 2; auto.
   apply storebytes_store. exact SB2.
-  simpl. apply Zdivide_plus_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
+  simpl. apply Z.divide_add_r. apply Zdivides_trans with 8; auto. exists 2; auto. exists 1; auto.
 Qed.
 
 Theorem storev_int64_split:
@@ -1676,7 +1676,7 @@ Variable b: block.
 Hypothesis ALLOC: alloc m1 lo hi = (m2, b).
 
 Theorem nextblock_alloc:
-  nextblock m2 = Psucc (nextblock m1).
+  nextblock m2 = Pos.succ (nextblock m1).
 Proof.
   injection ALLOC; intros. rewrite <- H0; auto.
 Qed.
@@ -1808,7 +1808,7 @@ Proof.
   subst b'. elimtype False. eauto with mem.
   rewrite pred_dec_true; auto.
   injection ALLOC; intros. rewrite <- H2; simpl.
-  rewrite PMap.gso. auto. rewrite H1. apply sym_not_equal; eauto with mem.
+  rewrite PMap.gso. auto. rewrite H1. apply not_eq_sym; eauto with mem.
   rewrite pred_dec_false. auto.
   eauto with mem.
 Qed.
@@ -2301,14 +2301,14 @@ Lemma getN_inj:
   mem_inj f m1 m2 ->
   f b1 = Some(b2, delta) ->
   forall n ofs,
-  range_perm m1 b1 ofs (ofs + Z_of_nat n) Cur Readable ->
+  range_perm m1 b1 ofs (ofs + Z.of_nat n) Cur Readable ->
   list_forall2 (memval_inject f)
                (getN n ofs (m1.(mem_contents)#b1))
                (getN n (ofs + delta) (m2.(mem_contents)#b2)).
 Proof.
   induction n; intros; simpl.
   constructor.
-  rewrite inj_S in H1.
+  rewrite Nat2Z.inj_succ in H1.
   constructor.
   eapply mi_memval; eauto.
   apply H1. omega.
@@ -2487,9 +2487,9 @@ Lemma storebytes_mapped_inj:
     /\ mem_inj f n1 n2.
 Proof.
   intros. inversion H.
-  assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Cur Writable).
-    replace (ofs + delta + Z_of_nat (length bytes2))
-       with ((ofs + Z_of_nat (length bytes1)) + delta).
+  assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z.of_nat (length bytes2)) Cur Writable).
+    replace (ofs + delta + Z.of_nat (length bytes2))
+       with ((ofs + Z.of_nat (length bytes1)) + delta).
     eapply range_perm_inj; eauto with mem.
     eapply storebytes_range_perm; eauto.
     rewrite (list_forall2_length H3). omega.
@@ -2557,7 +2557,7 @@ Lemma storebytes_outside_inj:
   (forall b' delta ofs',
     f b' = Some(b, delta) ->
     perm m1 b' ofs' Cur Readable ->
-    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
+    ofs <= ofs' + delta < ofs + Z.of_nat (length bytes2) -> False) ->
   storebytes m2 b ofs bytes2 = Some m2' ->
   mem_inj f m1 m2'.
 Proof.
@@ -2572,7 +2572,7 @@ Proof.
   rewrite PMap.gsspec. destruct (peq b2 b). subst b2.
   rewrite setN_outside. auto.
   destruct (zlt (ofs0 + delta) ofs); auto.
-  destruct (zle (ofs + Z_of_nat (length bytes2)) (ofs0 + delta)). omega.
+  destruct (zle (ofs + Z.of_nat (length bytes2)) (ofs0 + delta)). omega.
   byContradiction. eapply H0; eauto. omega.
   eauto with mem.
 Qed.
@@ -2975,7 +2975,7 @@ Theorem storebytes_outside_extends:
   forall m1 m2 b ofs bytes2 m2',
   extends m1 m2 ->
   storebytes m2 b ofs bytes2 = Some m2' ->
-  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) ->
+  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z.of_nat (length bytes2) -> False) ->
   extends m1 m2'.
 Proof.
   intros. inversion H. constructor.
@@ -3009,7 +3009,7 @@ Proof.
   eapply alloc_left_mapped_inj with (m1 := m1) (m2 := m2') (b2 := b) (delta := 0); eauto.
   eapply alloc_right_inj; eauto.
   eauto with mem.
-  red. intros. apply Zdivide_0.
+  red. intros. apply Z.divide_0_r.
   intros.
   eapply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto.
@@ -3419,8 +3419,8 @@ Theorem aligned_area_inject:
 Proof.
   intros.
   assert (P: al > 0) by omega.
-  assert (Q: Zabs al <= Zabs sz). apply Zdivide_bounds; auto. omega.
-  rewrite Zabs_eq in Q; try omega. rewrite Zabs_eq in Q; try omega.
+  assert (Q: Z.abs al <= Z.abs sz). apply Zdivide_bounds; auto. omega.
+  rewrite Z.abs_eq in Q; try omega. rewrite Z.abs_eq in Q; try omega.
   assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk).
     destruct H0. subst; exists Mint8unsigned; auto.
     destruct H0. subst; exists Mint16unsigned; auto.
@@ -3629,7 +3629,7 @@ Theorem storebytes_outside_inject:
   (forall b' delta ofs',
     f b' = Some(b, delta) ->
     perm m1 b' ofs' Cur Readable ->
-    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
+    ofs <= ofs' + delta < ofs + Z.of_nat (length bytes2) -> False) ->
   storebytes m2 b ofs bytes2 = Some m2' ->
   inject f m1 m2'.
 Proof.
@@ -3863,7 +3863,7 @@ Proof.
   auto.
   intros. apply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto. omega.
-  red; intros. apply Zdivide_0.
+  red; intros. apply Z.divide_0_r.
   intros. apply (valid_not_valid_diff m2 b2 b2); eauto with mem.
   intros [f' [A [B [C D]]]].
   exists f'; exists m2'; exists b2; auto.
@@ -4205,7 +4205,7 @@ Proof.
 (* perm inv *)
   unfold flat_inj; intros.
   destruct (plt b1 (nextblock m)); inv H0.
-  rewrite Zplus_0_r in H1; auto.
+  rewrite Z.add_0_r in H1; auto.
 Qed.
 
 Theorem empty_inject_neutral:
@@ -4231,7 +4231,7 @@ Proof.
   intros; red.
   eapply alloc_left_mapped_inj with (m1 := m) (b2 := b) (delta := 0).
   eapply alloc_right_inj; eauto. eauto. eauto with mem.
-  red. intros. apply Zdivide_0.
+  red. intros. apply Z.divide_0_r.
   intros.
   apply perm_implies with Freeable; auto with mem.
   eapply perm_alloc_2; eauto. omega.
@@ -4264,7 +4264,7 @@ Proof.
   unfold inject_neutral; intros.
   exploit drop_mapped_inj; eauto. apply flat_inj_no_overlap.
   unfold flat_inj. apply pred_dec_true; eauto.
-  repeat rewrite Zplus_0_r. intros [m'' [A B]]. congruence.
+  repeat rewrite Z.add_0_r. intros [m'' [A B]]. congruence.
 Qed.
 
 (** * Invariance properties between two memory states *)
@@ -4407,7 +4407,7 @@ Qed.
 Lemma storebytes_unchanged_on:
   forall m b ofs bytes m',
   storebytes m b ofs bytes = Some m' ->
-  (forall i, ofs <= i < ofs + Z_of_nat (length bytes) -> ~ P b i) ->
+  (forall i, ofs <= i < ofs + Z.of_nat (length bytes) -> ~ P b i) ->
   unchanged_on m m'.
 Proof.
   intros; constructor; intros.
@@ -4416,7 +4416,7 @@ Proof.
 - erewrite storebytes_mem_contents; eauto. rewrite PMap.gsspec.
   destruct (peq b0 b); auto. subst b0. apply setN_outside.
   destruct (zlt ofs0 ofs); auto.
-  destruct (zlt ofs0 (ofs + Z_of_nat (length bytes))); auto.
+  destruct (zlt ofs0 (ofs + Z.of_nat (length bytes))); auto.
   elim (H0 ofs0). omega. auto.
 Qed.
 
diff --git a/common/Memtype.v b/common/Memtype.v
index b055668c..ae4fa5fd 100644
--- a/common/Memtype.v
+++ b/common/Memtype.v
@@ -515,11 +515,11 @@ Axiom store_int16_sign_ext:
 
 Axiom range_perm_storebytes:
   forall m1 b ofs bytes,
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable ->
+  range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable ->
   { m2 : mem | storebytes m1 b ofs bytes = Some m2 }.
 Axiom storebytes_range_perm:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
-  range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable.
+  range_perm m1 b ofs (ofs + Z.of_nat (length bytes)) Cur Writable.
 Axiom perm_storebytes_1:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
   forall b' ofs' k p, perm m1 b' ofs' k p -> perm m2 b' ofs' k p.
@@ -561,21 +561,21 @@ Axiom store_storebytes:
 
 Axiom loadbytes_storebytes_same:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
-  loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes.
+  loadbytes m2 b ofs (Z.of_nat (length bytes)) = Some bytes.
 Axiom loadbytes_storebytes_other:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
   forall b' ofs' len,
   len >= 0 ->
   b' <> b
   \/ ofs' + len <= ofs
-  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  \/ ofs + Z.of_nat (length bytes) <= ofs' ->
   loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len.
 Axiom load_storebytes_other:
   forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 ->
   forall chunk b' ofs',
   b' <> b
   \/ ofs' + size_chunk chunk <= ofs
-  \/ ofs + Z_of_nat (length bytes) <= ofs' ->
+  \/ ofs + Z.of_nat (length bytes) <= ofs' ->
   load chunk m2 b' ofs' = load chunk m1 b' ofs'.
 
 (** Composing or decomposing [storebytes] operations at adjacent addresses. *)
@@ -583,14 +583,14 @@ Axiom load_storebytes_other:
 Axiom storebytes_concat:
   forall m b ofs bytes1 m1 bytes2 m2,
   storebytes m b ofs bytes1 = Some m1 ->
-  storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 ->
+  storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2 ->
   storebytes m b ofs (bytes1 ++ bytes2) = Some m2.
 Axiom storebytes_split:
   forall m b ofs bytes1 bytes2 m2,
   storebytes m b ofs (bytes1 ++ bytes2) = Some m2 ->
   exists m1,
      storebytes m b ofs bytes1 = Some m1
-  /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2.
+  /\ storebytes m1 b (ofs + Z.of_nat(length bytes1)) bytes2 = Some m2.
 
 (** ** Properties of [alloc]. *)
 
@@ -605,7 +605,7 @@ Axiom alloc_result:
 
 Axiom nextblock_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
-  nextblock m2 = Psucc (nextblock m1).
+  nextblock m2 = Pos.succ (nextblock m1).
 
 Axiom valid_block_alloc:
   forall m1 lo hi m2 b, alloc m1 lo hi = (m2, b) ->
@@ -867,7 +867,7 @@ Axiom storebytes_outside_extends:
   forall m1 m2 b ofs bytes2 m2',
   extends m1 m2 ->
   storebytes m2 b ofs bytes2 = Some m2' ->
-  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z_of_nat (length bytes2) -> False) ->
+  (forall ofs', perm m1 b ofs' Cur Readable -> ofs <= ofs' < ofs + Z.of_nat (length bytes2) -> False) ->
   extends m1 m2'.
 
 Axiom alloc_extends:
@@ -1113,7 +1113,7 @@ Axiom storebytes_outside_inject:
   (forall b' delta ofs',
     f b' = Some(b, delta) ->
     perm m1 b' ofs' Cur Readable ->
-    ofs <= ofs' + delta < ofs + Z_of_nat (length bytes2) -> False) ->
+    ofs <= ofs' + delta < ofs + Z.of_nat (length bytes2) -> False) ->
   storebytes m2 b ofs bytes2 = Some m2' ->
   inject f m1 m2'.
 
diff --git a/common/Separation.v b/common/Separation.v
index c27148aa..a9642d72 100644
--- a/common/Separation.v
+++ b/common/Separation.v
@@ -680,7 +680,7 @@ Lemma alloc_parallel_rule:
   Mem.alloc m2 0 sz2 = (m2', b2) ->
   (8 | delta) ->
   lo = delta ->
-  hi = delta + Zmax 0 sz1 ->
+  hi = delta + Z.max 0 sz1 ->
   0 <= sz2 <= Ptrofs.max_unsigned ->
   0 <= delta -> hi <= sz2 ->
   exists j',
@@ -740,7 +740,7 @@ Lemma free_parallel_rule:
   m2 |= range b2 0 lo ** range b2 hi sz2 ** minjection j m1 ** P ->
   Mem.free m1 b1 0 sz1 = Some m1' ->
   j b1 = Some (b2, delta) ->
-  lo = delta -> hi = delta + Zmax 0 sz1 ->
+  lo = delta -> hi = delta + Z.max 0 sz1 ->
   exists m2',
      Mem.free m2 b2 0 sz2 = Some m2'
   /\ m2' |= minjection j m1' ** P.
@@ -841,7 +841,7 @@ Proof.
 - eauto.
 - destruct (j b1) as [[b0 delta0]|] eqn:JB1.
 + erewrite H in H1 by eauto. inv H1. eauto.
-+ exploit H0; eauto. intros (X & Y). elim Y. apply Plt_le_trans with bound; auto.
++ exploit H0; eauto. intros (X & Y). elim Y. apply Pos.lt_le_trans with bound; auto.
 - eauto.
 - eauto.
 - eauto.
@@ -890,7 +890,7 @@ Lemma alloc_parallel_rule_2:
   Mem.alloc m2 0 sz2 = (m2', b2) ->
   (8 | delta) ->
   lo = delta ->
-  hi = delta + Zmax 0 sz1 ->
+  hi = delta + Z.max 0 sz1 ->
   0 <= sz2 <= Ptrofs.max_unsigned ->
   0 <= delta -> hi <= sz2 ->
   exists j',
diff --git a/common/Switch.v b/common/Switch.v
index 0df2bbc8..0ef91d60 100644
--- a/common/Switch.v
+++ b/common/Switch.v
@@ -123,8 +123,8 @@ Fixpoint validate_jumptable (cases: ZMap.t nat)
   match tbl with
   | nil => true
   | act :: rem =>
-      beq_nat act (ZMap.get n cases)
-      && validate_jumptable cases rem (Zsucc n)
+      Nat.eqb act (ZMap.get n cases)
+      && validate_jumptable cases rem (Z.succ n)
   end.
 
 Fixpoint validate (default: nat) (cases: table) (t: comptree)
@@ -133,9 +133,9 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree)
   | CTaction act =>
       match cases with
       | nil =>
-          beq_nat act default
+          Nat.eqb act default
       | (key1, act1) :: _ =>
-          zeq key1 lo && zeq lo hi && beq_nat act act1
+          zeq key1 lo && zeq lo hi && Nat.eqb act act1
       end
   | CTifeq pivot act t' =>
       zle 0 pivot && zlt pivot modulus &&
@@ -143,7 +143,7 @@ Fixpoint validate (default: nat) (cases: table) (t: comptree)
       | (None, _) =>
           false
       | (Some act', others) =>
-          beq_nat act act'
+          Nat.eqb act act'
           && validate default others t'
                       (refine_low_bound pivot lo)
                       (refine_high_bound pivot hi)
-- 
cgit