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.
---
 backend/Allocation.v      | 12 ++++++------
 backend/Allocproof.v      |  2 +-
 backend/Asmgenproof0.v    |  4 ++--
 backend/Bounds.v          | 34 ++++++++++++++++-----------------
 backend/CSE.v             |  6 +++---
 backend/CSEproof.v        | 10 +++++-----
 backend/Constpropproof.v  |  4 ++--
 backend/Deadcodeproof.v   | 18 +++++++++---------
 backend/Debugvarproof.v   | 12 ++++++------
 backend/Inlining.v        | 16 ++++++++--------
 backend/Inliningproof.v   | 28 +++++++++++++--------------
 backend/Inliningspec.v    | 22 +++++++++++-----------
 backend/Kildall.v         |  2 +-
 backend/Locations.v       | 10 +++++-----
 backend/NeedDomain.v      | 12 ++++++------
 backend/RTL.v             | 40 +++++++++++++++++++--------------------
 backend/RTLgen.v          | 18 +++++++++---------
 backend/RTLgenproof.v     |  4 ++--
 backend/SelectDivproof.v  | 48 +++++++++++++++++++++++------------------------
 backend/Selectionproof.v  |  6 +++---
 backend/Stackingproof.v   |  8 ++++----
 backend/Tunnelingproof.v  |  2 +-
 backend/Unusedglobproof.v | 14 +++++++-------
 backend/ValueAnalysis.v   |  4 ++--
 backend/ValueDomain.v     | 22 +++++++++++-----------
 25 files changed, 179 insertions(+), 179 deletions(-)

(limited to 'backend')

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 3ac99a47..cf62295d 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -404,11 +404,11 @@ Module OrderedEquation <: OrderedType.
     (OrderedLoc.lt (eloc x) (eloc y) \/ (eloc x = eloc y /\
     OrderedEqKind.lt (ekind x) (ekind y)))).
   Lemma eq_refl : forall x : t, eq x x.
-  Proof (@refl_equal t).
+  Proof (@eq_refl t).
   Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof (@sym_equal t).
+  Proof (@eq_sym t).
   Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof (@trans_equal t).
+  Proof (@eq_trans t).
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Proof.
     unfold lt; intros.
@@ -466,11 +466,11 @@ Module OrderedEquation' <: OrderedType.
     (Plt (ereg x) (ereg y) \/ (ereg x = ereg y /\
     OrderedEqKind.lt (ekind x) (ekind y)))).
   Lemma eq_refl : forall x : t, eq x x.
-  Proof (@refl_equal t).
+  Proof (@eq_refl t).
   Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof (@sym_equal t).
+  Proof (@eq_sym t).
   Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof (@trans_equal t).
+  Proof (@eq_trans t).
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Proof.
     unfold lt; intros.
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 6c10d27f..4b75e34d 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -2444,7 +2444,7 @@ Proof.
 (* internal function *)
 - monadInv FUN. simpl in *.
   destruct (transf_function_inv _ _ EQ).
-  exploit Mem.alloc_extends; eauto. apply Zle_refl. rewrite H8; apply Zle_refl.
+  exploit Mem.alloc_extends; eauto. apply Z.le_refl. rewrite H8; apply Z.le_refl.
   intros [m'' [U V]].
   assert (WTRS: wt_regset env (init_regs args (fn_params f))).
   { apply wt_init_regs. inv H0. rewrite wt_params. rewrite H9. auto. }
diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v
index 0250628b..f6f03868 100644
--- a/backend/Asmgenproof0.v
+++ b/backend/Asmgenproof0.v
@@ -103,7 +103,7 @@ Lemma nextinstr_set_preg:
   (nextinstr (rs#(preg_of m) <- v))#PC = Val.offset_ptr rs#PC Ptrofs.one.
 Proof.
   intros. unfold nextinstr. rewrite Pregmap.gss.
-  rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_PC.
+  rewrite Pregmap.gso. auto. apply not_eq_sym. apply preg_of_not_PC.
 Qed.
 
 Lemma undef_regs_other:
@@ -211,7 +211,7 @@ Lemma agree_set_mreg:
   agree (Regmap.set r v ms) sp rs'.
 Proof.
   intros. destruct H. split; auto.
-  rewrite H1; auto. apply sym_not_equal. apply preg_of_not_SP.
+  rewrite H1; auto. apply not_eq_sym. apply preg_of_not_SP.
   intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence.
   rewrite H1. auto. apply preg_of_data.
   red; intros; elim n. eapply preg_of_injective; eauto.
diff --git a/backend/Bounds.v b/backend/Bounds.v
index 93a4b504..fa695234 100644
--- a/backend/Bounds.v
+++ b/backend/Bounds.v
@@ -136,7 +136,7 @@ Definition slots_of_instr (i: instruction) : list (slot * Z * typ) :=
   end.
 
 Definition max_over_list {A: Type} (valu: A -> Z) (l: list A) : Z :=
-  List.fold_left (fun m l => Zmax m (valu l)) l 0.
+  List.fold_left (fun m l => Z.max m (valu l)) l 0.
 
 Definition max_over_instrs (valu: instruction -> Z) : Z :=
   max_over_list valu f.(fn_code).
@@ -161,10 +161,10 @@ Lemma max_over_list_pos:
   max_over_list valu l >= 0.
 Proof.
   intros until valu. unfold max_over_list.
-  assert (forall l z, fold_left (fun x y => Zmax x (valu y)) l z >= z).
+  assert (forall l z, fold_left (fun x y => Z.max x (valu y)) l z >= z).
   induction l; simpl; intros.
-  omega. apply Zge_trans with (Zmax z (valu a)).
-  auto. apply Zle_ge. apply Zmax1. auto.
+  omega. apply Zge_trans with (Z.max z (valu a)).
+  auto. apply Z.le_ge. apply Z.le_max_l. auto.
 Qed.
 
 Lemma max_over_slots_of_funct_pos:
@@ -225,18 +225,18 @@ Qed.
 Program Definition function_bounds := {|
   used_callee_save := RegSet.elements record_regs_of_function;
   bound_local := max_over_slots_of_funct local_slot;
-  bound_outgoing := Zmax (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot);
-  bound_stack_data := Zmax f.(fn_stacksize) 0
+  bound_outgoing := Z.max (max_over_instrs outgoing_space) (max_over_slots_of_funct outgoing_slot);
+  bound_stack_data := Z.max f.(fn_stacksize) 0
 |}.
 Next Obligation.
   apply max_over_slots_of_funct_pos.
 Qed.
 Next Obligation.
-  apply Zle_ge. eapply Zle_trans. 2: apply Zmax2.
-  apply Zge_le. apply max_over_slots_of_funct_pos.
+  apply Z.le_ge. eapply Z.le_trans. 2: apply Z.le_max_r.
+  apply Z.ge_le. apply max_over_slots_of_funct_pos.
 Qed.
 Next Obligation.
-  apply Zle_ge. apply Zmax2.
+  apply Z.le_ge. apply Z.le_max_r.
 Qed.
 Next Obligation.
   generalize (RegSet.elements_3w record_regs_of_function).
@@ -304,15 +304,15 @@ Lemma max_over_list_bound:
 Proof.
   intros until x. unfold max_over_list.
   assert (forall c z,
-            let f := fold_left (fun x y => Zmax x (valu y)) c z in
+            let f := fold_left (fun x y => Z.max x (valu y)) c z in
             z <= f /\ (In x c -> valu x <= f)).
     induction c; simpl; intros.
     split. omega. tauto.
-    elim (IHc (Zmax z (valu a))); intros.
-    split. apply Zle_trans with (Zmax z (valu a)). apply Zmax1. auto.
+    elim (IHc (Z.max z (valu a))); intros.
+    split. apply Z.le_trans with (Z.max z (valu a)). apply Z.le_max_l. auto.
     intro H1; elim H1; intro.
-    subst a. apply Zle_trans with (Zmax z (valu x)).
-    apply Zmax2. auto. auto.
+    subst a. apply Z.le_trans with (Z.max z (valu x)).
+    apply Z.le_max_r. auto. auto.
   intro. elim (H l 0); intros. auto.
 Qed.
 
@@ -329,7 +329,7 @@ Lemma max_over_slots_of_funct_bound:
   valu s <= max_over_slots_of_funct valu.
 Proof.
   intros. unfold max_over_slots_of_funct.
-  apply Zle_trans with (max_over_slots_of_instr valu i).
+  apply Z.le_trans with (max_over_slots_of_instr valu i).
   unfold max_over_slots_of_instr. apply max_over_list_bound. auto.
   apply max_over_instrs_bound. auto.
 Qed.
@@ -447,9 +447,9 @@ Proof.
 Local Opaque mreg_type.
   induction l as [ | r l]; intros; simpl.
 - omega.
-- eapply Zle_trans. 2: apply IHl.
+- eapply Z.le_trans. 2: apply IHl.
   generalize (AST.typesize_pos (mreg_type r)); intros.
-  apply Zle_trans with (align ofs (AST.typesize (mreg_type r))).
+  apply Z.le_trans with (align ofs (AST.typesize (mreg_type r))).
   apply align_le; auto.
   omega.
 Qed.
diff --git a/backend/CSE.v b/backend/CSE.v
index 4fa1bd6c..bc3fdba5 100644
--- a/backend/CSE.v
+++ b/backend/CSE.v
@@ -50,7 +50,7 @@ Definition valnum_reg (n: numbering) (r: reg) : numbering * valnum :=
   | Some v => (n, v)
   | None   =>
       let v := n.(num_next) in
-      ( {| num_next := Psucc v;
+      ( {| num_next := Pos.succ v;
            num_eqs  := n.(num_eqs);
            num_reg  := PTree.set r v n.(num_reg);
            num_val  := PMap.set v (r :: nil) n.(num_val) |},
@@ -161,7 +161,7 @@ Definition add_rhs (n: numbering) (rd: reg) (rh: rhs) : numbering :=
          num_reg  := PTree.set rd vres n.(num_reg);
          num_val  := update_reg n rd vres |}
   | None =>
-      {| num_next := Psucc n.(num_next);
+      {| num_next := Pos.succ n.(num_next);
          num_eqs  := Eq n.(num_next) true rh :: n.(num_eqs);
          num_reg  := PTree.set rd n.(num_next) n.(num_reg);
          num_val  := update_reg n rd n.(num_next) |}
@@ -331,7 +331,7 @@ Definition shift_memcpy_eq (src sz delta: Z) (e: equation) :=
       let j := i + delta in
       if zle src i
       && zle (i + size_chunk chunk) (src + sz)
-      && zeq (Zmod delta (align_chunk chunk)) 0
+      && zeq (Z.modulo delta (align_chunk chunk)) 0
       && zle 0 j
       && zle j Ptrofs.max_unsigned
       then Some(Eq l strict (Load chunk (Ainstack (Ptrofs.repr j)) nil))
diff --git a/backend/CSEproof.v b/backend/CSEproof.v
index 8516e384..d6bde348 100644
--- a/backend/CSEproof.v
+++ b/backend/CSEproof.v
@@ -35,8 +35,8 @@ Remark wf_equation_incr:
   wf_equation next1 e -> Ple next1 next2 -> wf_equation next2 e.
 Proof.
   unfold wf_equation; intros; destruct e. destruct H. split.
-  apply Plt_le_trans with next1; auto.
-  red; intros. apply Plt_le_trans with next1; auto. apply H1; auto.
+  apply Pos.lt_le_trans with next1; auto.
+  red; intros. apply Pos.lt_le_trans with next1; auto. apply H1; auto.
 Qed.
 
 (** Extensionality with respect to valuations. *)
@@ -95,7 +95,7 @@ Proof.
 - auto.
 - apply equation_holds_exten. auto.
   eapply wf_equation_incr; eauto with cse.
-- rewrite AGREE. eauto. eapply Plt_le_trans; eauto. eapply wf_num_reg; eauto.
+- rewrite AGREE. eauto. eapply Pos.lt_le_trans; eauto. eapply wf_num_reg; eauto.
 Qed.
 
 End EXTEN.
@@ -523,7 +523,7 @@ Proof.
   exists valu3. constructor; simpl; intros.
 + constructor; simpl; intros; eauto with cse.
   destruct H4; eauto with cse. subst e. split.
-  eapply Plt_le_trans; eauto.
+  eapply Pos.lt_le_trans; eauto.
   red; simpl; intros. auto.
 + destruct H4; eauto with cse. subst eq. apply eq_holds_lessdef with (Val.load_result chunk rs#src).
   apply load_eval_to with a. rewrite <- Q; auto.
@@ -1187,7 +1187,7 @@ Proof.
 - (* internal function *)
   monadInv TFD. unfold transf_function in EQ. fold (analyze cu f) in EQ.
   destruct (analyze cu f) as [approx|] eqn:?; inv EQ.
-  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 (m'' & A & B).
   econstructor; split.
   eapply exec_function_internal; simpl; eauto.
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v
index b14c4be0..e28519ca 100644
--- a/backend/Constpropproof.v
+++ b/backend/Constpropproof.v
@@ -493,7 +493,7 @@ Opaque builtin_strength_reduction.
   assert (C: cmatch (eval_condition cond rs ## args m) ac)
   by (eapply eval_static_condition_sound; eauto with va).
   rewrite H0 in C.
-  generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (refl_equal _)).
+  generalize (cond_strength_reduction_correct bc ae rs m EM cond args (aregs ae args) (eq_refl _)).
   destruct (cond_strength_reduction cond args (aregs ae args)) as [cond' args'].
   intros EV1 TCODE.
   left; exists O; exists (State s' (transf_function (romem_for cu) f) (Vptr sp0 Ptrofs.zero) (if b then ifso else ifnot) rs' m'); split.
@@ -532,7 +532,7 @@ Opaque builtin_strength_reduction.
   destruct or; simpl; auto.
 
 - (* internal function *)
-  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
+  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros [m2' [A B]].
   simpl. unfold transf_function.
   left; exists O; econstructor; split.
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v
index e23fdfd3..ca6ad649 100644
--- a/backend/Deadcodeproof.v
+++ b/backend/Deadcodeproof.v
@@ -69,7 +69,7 @@ Proof.
 - replace ofs with (ofs + 0) by omega. eapply mi_perm; eauto. auto.
 - eauto.
 - exploit mi_memval; eauto. unfold inject_id; eauto.
-  rewrite Zplus_0_r. auto.
+  rewrite Z.add_0_r. auto.
 - auto.
 Qed.
 
@@ -79,9 +79,9 @@ Lemma magree_extends:
   magree m1 m2 P -> Mem.extends m1 m2.
 Proof.
   intros. destruct H0. constructor; auto. constructor; unfold inject_id; intros.
-- inv H0. rewrite Zplus_0_r. eauto.
-- inv H0. apply Zdivide_0.
-- inv H0. rewrite Zplus_0_r. eapply ma_memval0; eauto.
+- inv H0. rewrite Z.add_0_r. eauto.
+- inv H0. apply Z.divide_0_r.
+- inv H0. rewrite Z.add_0_r. eapply ma_memval0; eauto.
 Qed.
 
 Lemma magree_loadbytes:
@@ -97,7 +97,7 @@ Proof.
   {
     induction n; intros; simpl.
     constructor.
-    rewrite inj_S in H. constructor.
+    rewrite Nat2Z.inj_succ in H. constructor.
     apply H. omega.
     apply IHn. intros; apply H; omega.
   }
@@ -131,7 +131,7 @@ Lemma magree_storebytes_parallel:
   magree m1 m2 P ->
   Mem.storebytes m1 b ofs bytes1 = Some m1' ->
   (forall b' i, Q b' i ->
-                b' <> b \/ i < ofs \/ ofs + Z_of_nat (length bytes1) <= i ->
+                b' <> b \/ i < ofs \/ ofs + Z.of_nat (length bytes1) <= i ->
                 P b' i) ->
   list_forall2 memval_lessdef bytes1 bytes2 ->
   exists m2', Mem.storebytes m2 b ofs bytes2 = Some m2' /\ magree m1' m2' Q.
@@ -146,7 +146,7 @@ Proof.
   {
     induction 1; intros; simpl.
   - apply H; auto. simpl. omega.
-  - simpl length in H1; rewrite inj_S in H1.
+  - simpl length in H1; rewrite Nat2Z.inj_succ in H1.
     apply IHlist_forall2; auto.
     intros. rewrite ! ZMap.gsspec. destruct (ZIndexed.eq i p). auto.
     apply H1; auto. unfold ZIndexed.t in *; omega.
@@ -200,7 +200,7 @@ Lemma magree_storebytes_left:
   forall m1 m2 P b ofs bytes1 m1',
   magree m1 m2 P ->
   Mem.storebytes m1 b ofs bytes1 = Some m1' ->
-  (forall i, ofs <= i < ofs + Z_of_nat (length bytes1) -> ~(P b i)) ->
+  (forall i, ofs <= i < ofs + Z.of_nat (length bytes1) -> ~(P b i)) ->
   magree m1' m2 P.
 Proof.
   intros. constructor; intros.
@@ -1081,7 +1081,7 @@ Ltac UseTransfer :=
 - (* internal function *)
   monadInv FUN. generalize EQ. unfold transf_function. fold (vanalyze cu f). intros EQ'.
   destruct (analyze (vanalyze cu f) f) as [an|] eqn:AN; inv EQ'.
-  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 (tm' & A & B).
   econstructor; split.
   econstructor; simpl; eauto.
diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v
index 0b8ff3c7..d31c63ec 100644
--- a/backend/Debugvarproof.v
+++ b/backend/Debugvarproof.v
@@ -157,11 +157,11 @@ Proof.
 - intuition congruence.
 - destruct (Pos.compare_spec v v0); simpl in H1.
 + subst v0. destruct H1. inv H1; auto. right; split.
-  apply sym_not_equal. apply Plt_ne. eapply H; eauto.
+  apply not_eq_sym. apply Plt_ne. eapply H; eauto.
   auto.
 + destruct H1. inv H1; auto.
-  destruct H1. inv H1. right; split; auto. apply sym_not_equal. apply Plt_ne. auto.
-  right; split; auto. apply sym_not_equal. apply Plt_ne. apply Plt_trans with v0; eauto.
+  destruct H1. inv H1. right; split; auto. apply not_eq_sym. apply Plt_ne. auto.
+  right; split; auto. apply not_eq_sym. apply Plt_ne. apply Plt_trans with v0; eauto.
 + destruct H1. inv H1. right; split; auto. apply Plt_ne. auto.
   destruct IHwf_avail as [A | [A B]]; auto.
 Qed.
@@ -211,9 +211,9 @@ Proof.
   induction 1; simpl; intros.
 - contradiction.
 - destruct (Pos.compare_spec v v0); simpl in H1.
-+ subst v0. split; auto. apply sym_not_equal; apply Plt_ne; eauto.
-+ destruct H1. inv H1. split; auto. apply sym_not_equal; apply Plt_ne; eauto.
-  split; auto. apply sym_not_equal; apply Plt_ne. apply Plt_trans with v0; eauto.
++ subst v0. split; auto. apply not_eq_sym; apply Plt_ne; eauto.
++ destruct H1. inv H1. split; auto. apply not_eq_sym; apply Plt_ne; eauto.
+  split; auto. apply not_eq_sym; apply Plt_ne. apply Plt_trans with v0; eauto.
 + destruct H1. inv H1. split; auto. apply Plt_ne; auto.
   destruct IHwf_avail as [A B] ; auto.
 Qed.
diff --git a/backend/Inlining.v b/backend/Inlining.v
index 17139dbd..91cc119d 100644
--- a/backend/Inlining.v
+++ b/backend/Inlining.v
@@ -113,7 +113,7 @@ Program Definition add_instr (i: instruction): mon node :=
   fun s =>
     let pc := s.(st_nextnode) in
     R pc
-      (mkstate s.(st_nextreg) (Psucc pc) (PTree.set pc i s.(st_code)) s.(st_stksize))
+      (mkstate s.(st_nextreg) (Pos.succ pc) (PTree.set pc i s.(st_code)) s.(st_stksize))
       _.
 Next Obligation.
   intros; constructor; simpl; xomega.
@@ -122,7 +122,7 @@ Qed.
 Program Definition reserve_nodes (numnodes: positive): mon positive :=
   fun s =>
     R s.(st_nextnode)
-      (mkstate s.(st_nextreg) (Pplus s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize))
+      (mkstate s.(st_nextreg) (Pos.add s.(st_nextnode) numnodes) s.(st_code) s.(st_stksize))
       _.
 Next Obligation.
   intros; constructor; simpl; xomega.
@@ -131,7 +131,7 @@ Qed.
 Program Definition reserve_regs (numregs: positive): mon positive :=
   fun s =>
     R s.(st_nextreg)
-      (mkstate (Pplus s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize))
+      (mkstate (Pos.add s.(st_nextreg) numregs) s.(st_nextnode) s.(st_code) s.(st_stksize))
       _.
 Next Obligation.
   intros; constructor; simpl; xomega.
@@ -140,7 +140,7 @@ Qed.
 Program Definition request_stack (sz: Z): mon unit :=
   fun s =>
     R tt
-      (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Zmax s.(st_stksize) sz))
+      (mkstate s.(st_nextreg) s.(st_nextnode) s.(st_code) (Z.max s.(st_stksize) sz))
       _.
 Next Obligation.
   intros; constructor; simpl; xomega.
@@ -181,7 +181,7 @@ Record context: Type := mkcontext {
 
 (** The following functions "shift" (relocate) PCs, registers, operations, etc. *)
 
-Definition shiftpos (p amount: positive) := Ppred (Pplus p amount).
+Definition shiftpos (p amount: positive) := Pos.pred (Pos.add p amount).
 
 Definition spc (ctx: context) (pc: node) := shiftpos pc ctx.(dpc).
 
@@ -220,7 +220,7 @@ Definition initcontext (dpc dreg nreg: positive) (sz: Z) :=
      dreg := dreg;
      dstk := 0;
      mreg := nreg;
-     mstk := Zmax sz 0;
+     mstk := Z.max sz 0;
      retinfo := None |}.
 
 (** The context used to inline a call to another function. *)
@@ -237,7 +237,7 @@ Definition callcontext (ctx: context)
      dreg := dreg;
      dstk := align (ctx.(dstk) + ctx.(mstk)) (min_alignment sz);
      mreg := nreg;
-     mstk := Zmax sz 0;
+     mstk := Z.max sz 0;
      retinfo := Some (spc ctx retpc, sreg ctx retreg) |}.
 
 (** The context used to inline a tail call to another function. *)
@@ -247,7 +247,7 @@ Definition tailcontext (ctx: context) (dpc dreg nreg: positive) (sz: Z) :=
      dreg := dreg;
      dstk := align ctx.(dstk) (min_alignment sz);
      mreg := nreg;
-     mstk := Zmax sz 0;
+     mstk := Z.max sz 0;
      retinfo := ctx.(retinfo) |}.
 
 (** ** Recursive expansion and copying of a CFG *)
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v
index c3b0cfc3..2dcb8956 100644
--- a/backend/Inliningproof.v
+++ b/backend/Inliningproof.v
@@ -184,7 +184,7 @@ Proof.
   unfold agree_regs; intros. destruct H. split; intros.
   rewrite H0. auto.
   apply shiftpos_above.
-  eapply Plt_le_trans. apply shiftpos_below. xomega.
+  eapply Pos.lt_le_trans. apply shiftpos_below. xomega.
   apply H1; auto.
 Qed.
 
@@ -242,7 +242,7 @@ Proof.
   split. destruct H3 as [[P Q] | [P Q]].
   subst a1. eapply agree_set_reg_undef; eauto.
   eapply agree_set_reg; eauto. rewrite C; auto.  apply context_below_lt; auto.
-  intros. rewrite Regmap.gso. auto. apply sym_not_equal. eapply sreg_below_diff; eauto.
+  intros. rewrite Regmap.gso. auto. apply not_eq_sym. eapply sreg_below_diff; eauto.
   destruct H2; discriminate.
 Qed.
 
@@ -290,10 +290,10 @@ Lemma range_private_alloc_left:
   Mem.alloc m 0 sz = (m1, sp) ->
   F1 sp = Some(sp', base) ->
   (forall b, b <> sp -> F1 b = F b) ->
-  range_private F1 m1 m' sp' (base + Zmax sz 0) hi.
+  range_private F1 m1 m' sp' (base + Z.max sz 0) hi.
 Proof.
   intros; red; intros.
-  exploit (H ofs). generalize (Zmax2 sz 0). omega. intros [A B].
+  exploit (H ofs). generalize (Z.le_max_r sz 0). omega. intros [A B].
   split; auto. intros; red; intros.
   exploit Mem.perm_alloc_inv; eauto.
   destruct (eq_block b sp); intros.
@@ -304,14 +304,14 @@ Qed.
 
 Lemma range_private_free_left:
   forall F m m' sp base sz hi b m1,
-  range_private F m m' sp (base + Zmax sz 0) hi ->
+  range_private F m m' sp (base + Z.max sz 0) hi ->
   Mem.free m b 0 sz = Some m1 ->
   F b = Some(sp, base) ->
   Mem.inject F m m' ->
   range_private F m1 m' sp base hi.
 Proof.
   intros; red; intros.
-  destruct (zlt ofs (base + Zmax sz 0)) as [z|z].
+  destruct (zlt ofs (base + Z.max sz 0)) as [z|z].
   red; split.
   replace ofs with ((ofs - base) + base) by omega.
   eapply Mem.perm_inject; eauto.
@@ -560,8 +560,8 @@ Lemma match_stacks_bound:
 Proof.
   intros. inv H.
   apply match_stacks_nil with bound0. auto. eapply Ple_trans; eauto.
-  eapply match_stacks_cons; eauto. eapply Plt_le_trans; eauto.
-  eapply match_stacks_untailcall; eauto. eapply Plt_le_trans; eauto.
+  eapply match_stacks_cons; eauto. eapply Pos.lt_le_trans; eauto.
+  eapply match_stacks_untailcall; eauto. eapply Pos.lt_le_trans; eauto.
 Qed.
 
 Variable F1: meminj.
@@ -602,7 +602,7 @@ Proof.
   (* nil *)
   apply match_stacks_nil with (bound1 := bound1).
   inv MG. constructor; auto.
-  intros. apply IMAGE with delta. eapply INJ; eauto. eapply Plt_le_trans; eauto.
+  intros. apply IMAGE with delta. eapply INJ; eauto. eapply Pos.lt_le_trans; eauto.
   auto. auto.
   (* cons *)
   apply match_stacks_cons with (fenv := fenv) (ctx := ctx); auto.
@@ -768,8 +768,8 @@ Proof.
     destruct (zle sz 4). omegaContradiction.
     auto.
   destruct chunk; simpl in *; auto.
-  apply Zone_divide.
-  apply Zone_divide.
+  apply Z.divide_1_l.
+  apply Z.divide_1_l.
   apply H2; omega.
   apply H2; omega.
 Qed.
@@ -845,7 +845,7 @@ Proof.
   intros. inv H.
   (* base *)
   eapply match_stacks_inside_base; eauto. congruence.
-  rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Zdivide_0.
+  rewrite H1. rewrite DSTK. apply align_unchanged. apply min_alignment_pos. apply Z.divide_0_r.
   (* inlined *)
   assert (dstk ctx <= dstk ctx'). rewrite H1. apply align_le. apply min_alignment_pos.
   eapply match_stacks_inside_inlined; eauto.
@@ -1164,7 +1164,7 @@ Proof.
   assert (TR: tr_function prog f f').
   { eapply tr_function_linkorder; eauto. }
   inversion TR; subst.
-  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl.
+  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl.
     instantiate (1 := fn_stacksize f'). inv H1. xomega.
   intros [F' [m1' [sp' [A [B [C [D E]]]]]]].
   left; econstructor; split.
@@ -1203,7 +1203,7 @@ Proof.
     (* sp' is valid *)
     instantiate (1 := sp'). auto.
     (* offset is representable *)
-    instantiate (1 := dstk ctx). generalize (Zmax2 (fn_stacksize f) 0). omega.
+    instantiate (1 := dstk ctx). generalize (Z.le_max_r (fn_stacksize f) 0). omega.
     (* size of target block is representable *)
     intros. right. exploit SSZ2; eauto with mem. inv FB; omega.
     (* we have full permissions on sp' at and above dstk ctx *)
diff --git a/backend/Inliningspec.v b/backend/Inliningspec.v
index d79132d6..6e8a94a6 100644
--- a/backend/Inliningspec.v
+++ b/backend/Inliningspec.v
@@ -105,7 +105,7 @@ Proof.
 Qed.
 
 Lemma shiftpos_below:
-  forall x n, Plt (shiftpos x n) (Pplus x n).
+  forall x n, Plt (shiftpos x n) (Pos.add x n).
 Proof.
   intros. unfold Plt; zify. rewrite shiftpos_eq. omega.
 Qed.
@@ -250,7 +250,7 @@ Section INLINING_SPEC.
 Variable fenv: funenv.
 
 Definition context_below (ctx1 ctx2: context): Prop :=
-  Ple (Pplus ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg).
+  Ple (Pos.add ctx1.(dreg) ctx1.(mreg)) ctx2.(dreg).
 
 Definition context_stack_call (ctx1 ctx2: context): Prop :=
   ctx1.(mstk) >= 0 /\ ctx1.(dstk) + ctx1.(mstk) <= ctx2.(dstk).
@@ -331,7 +331,7 @@ with tr_funbody: context -> function -> code -> Prop :=
   | tr_funbody_intro: forall ctx f c,
       (forall r, In r f.(fn_params) -> Ple r ctx.(mreg)) ->
       (forall pc i, f.(fn_code)!pc = Some i -> tr_instr ctx pc i c) ->
-      ctx.(mstk) = Zmax f.(fn_stacksize) 0 ->
+      ctx.(mstk) = Z.max f.(fn_stacksize) 0 ->
       (min_alignment f.(fn_stacksize) | ctx.(dstk)) ->
       ctx.(dstk) >= 0 -> ctx.(dstk) + ctx.(mstk) <= stacksize ->
       tr_funbody ctx f c.
@@ -451,9 +451,9 @@ Hypothesis rec_spec:
   fenv_agree fe' ->
   Ple (ctx.(dpc) + max_pc_function f) s.(st_nextnode) ->
   ctx.(mreg) = max_reg_function f ->
-  Ple (Pplus ctx.(dreg) ctx.(mreg)) s.(st_nextreg) ->
+  Ple (Pos.add ctx.(dreg) ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 ->
-  ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
+  ctx.(mstk) = Z.max (fn_stacksize f) 0 ->
   (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
@@ -599,7 +599,7 @@ Proof.
     elim H12. change pc with (fst (pc, instr0)). apply List.in_map; auto.
   (* older pc *)
   inv_incr. eapply IHl; eauto.
-  intros. eapply Plt_le_trans. eapply H2. right; eauto. xomega.
+  intros. eapply Pos.lt_le_trans. eapply H2. right; eauto. xomega.
   intros; eapply Ple_trans; eauto.
   intros. apply H7; auto. xomega.
 Qed.
@@ -611,7 +611,7 @@ Lemma expand_cfg_rec_spec:
   ctx.(mreg) = max_reg_function f ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 ->
-  ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
+  ctx.(mstk) = Z.max (fn_stacksize f) 0 ->
   (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
@@ -629,13 +629,13 @@ Proof.
   intros.
     assert (Ple pc0 (max_pc_function f)).
       eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.
-      eapply Plt_le_trans. apply shiftpos_below. subst s0; simpl; xomega.
+      eapply Pos.lt_le_trans. apply shiftpos_below. subst s0; simpl; xomega.
   subst s0; simpl; auto.
   intros. apply H8; auto. subst s0; simpl in H11; xomega.
   intros. apply H8. apply shiftpos_above.
   assert (Ple pc0 (max_pc_function f)).
     eapply max_pc_function_sound. eapply PTree.elements_complete; eauto.
-  eapply Plt_le_trans. apply shiftpos_below. inversion i; xomega.
+  eapply Pos.lt_le_trans. apply shiftpos_below. inversion i; xomega.
   apply PTree.elements_correct; auto.
   auto. auto. auto.
   inversion INCR0. subst s0; simpl in STKSIZE; xomega.
@@ -664,7 +664,7 @@ Lemma expand_cfg_spec:
   ctx.(mreg) = max_reg_function f ->
   Ple (ctx.(dreg) + ctx.(mreg)) s.(st_nextreg) ->
   ctx.(mstk) >= 0 ->
-  ctx.(mstk) = Zmax (fn_stacksize f) 0 ->
+  ctx.(mstk) = Z.max (fn_stacksize f) 0 ->
   (min_alignment (fn_stacksize f) | ctx.(dstk)) ->
   ctx.(dstk) >= 0 ->
   s'.(st_stksize) <= stacksize ->
@@ -724,7 +724,7 @@ Opaque initstate.
     unfold ctx; rewrite <- H1; rewrite <- H2; rewrite <- H3; simpl. xomega.
     unfold ctx; rewrite <- H0; rewrite <- H1; simpl. xomega.
     simpl. xomega.
-    simpl. apply Zdivide_0.
+    simpl. apply Z.divide_0_r.
     simpl. omega.
   simpl. omega.
   simpl. split; auto. destruct INCR2. destruct INCR1. destruct INCR0. destruct INCR.
diff --git a/backend/Kildall.v b/backend/Kildall.v
index a2b49d56..8e712c05 100644
--- a/backend/Kildall.v
+++ b/backend/Kildall.v
@@ -1373,7 +1373,7 @@ Proof.
   replace (st1.(aval)!!pc) with res!!pc. fold l.
   destruct (basic_block_map s) eqn:BB.
   rewrite D. simpl. rewrite INV1. apply L.top_ge. auto. tauto.
-  elim (C H0 (refl_equal _)). intros X Y. rewrite Y. apply L.refl_ge.
+  elim (C H0 (eq_refl _)). intros X Y. rewrite Y. apply L.refl_ge.
   elim (U pc); intros E F. rewrite F. reflexivity.
   destruct (In_dec peq pc (successors instr)).
   right. eapply no_self_loop; eauto.
diff --git a/backend/Locations.v b/backend/Locations.v
index ca148761..c437df5d 100644
--- a/backend/Locations.v
+++ b/backend/Locations.v
@@ -471,11 +471,11 @@ Module OrderedLoc <: OrderedType.
         (ofs1 < ofs2 \/ (ofs1 = ofs2 /\ OrderedTyp.lt ty1 ty2)))
     end.
   Lemma eq_refl : forall x : t, eq x x.
-  Proof (@refl_equal t).
+  Proof (@eq_refl t).
   Lemma eq_sym : forall x y : t, eq x y -> eq y x.
-  Proof (@sym_equal t).
+  Proof (@eq_sym t).
   Lemma eq_trans : forall x y z : t, eq x y -> eq y z -> eq x z.
-  Proof (@trans_equal t).
+  Proof (@eq_trans t).
   Lemma lt_trans : forall x y z : t, lt x y -> lt y z -> lt x z.
   Proof.
     unfold lt; intros.
@@ -542,12 +542,12 @@ Module OrderedLoc <: OrderedType.
     intros.
     destruct l as [mr | sl ofs ty]; destruct l' as [mr' | sl' ofs' ty']; simpl in *; auto.
     - assert (IndexedMreg.index mr <> IndexedMreg.index mr').
-      { destruct H. apply sym_not_equal. apply Plt_ne; auto. apply Plt_ne; auto. }
+      { destruct H. apply not_eq_sym. apply Plt_ne; auto. apply Plt_ne; auto. }
       congruence.
     - assert (RANGE: forall ty, 1 <= typesize ty <= 2).
       { intros; unfold typesize. destruct ty0; omega.  }
       destruct H.
-      + destruct H. left. apply sym_not_equal. apply OrderedSlot.lt_not_eq; auto.
+      + destruct H. left. apply not_eq_sym. apply OrderedSlot.lt_not_eq; auto.
         destruct H. right.
         destruct H0. right. generalize (RANGE ty'); omega.
         destruct H0.
diff --git a/backend/NeedDomain.v b/backend/NeedDomain.v
index 8e8b9c0b..d431f3d8 100644
--- a/backend/NeedDomain.v
+++ b/backend/NeedDomain.v
@@ -329,7 +329,7 @@ Lemma eqmod_iagree:
 Proof.
   intros. set (p := nat_of_Z (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
   rewrite EQ in H; rewrite <- two_power_nat_two_p in H.
   red; intros. rewrite ! Int.testbit_repr by auto.
   destruct (zlt i (Int.size m)).
@@ -347,7 +347,7 @@ Lemma iagree_eqmod:
 Proof.
   intros. set (p := nat_of_Z (Int.size m)).
   generalize (Int.size_range m); intros RANGE.
-  assert (EQ: Int.size m = Z_of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
+  assert (EQ: Int.size m = Z.of_nat p). { symmetry; apply nat_of_Z_eq. omega. }
   rewrite EQ; rewrite <- two_power_nat_two_p.
   apply Int.eqmod_same_bits. intros. apply H. omega.
   unfold complete_mask. rewrite Int.bits_zero_ext by omega.
@@ -829,7 +829,7 @@ Let weak_valid_pointer_no_overflow:
   Mem.weak_valid_pointer m1 b1 (Ptrofs.unsigned ofs) = true ->
   0 <= Ptrofs.unsigned ofs + Ptrofs.unsigned (Ptrofs.repr delta) <= Ptrofs.max_unsigned.
 Proof.
-  unfold inject_id; intros. inv H. rewrite Zplus_0_r. apply Ptrofs.unsigned_range_2.
+  unfold inject_id; intros. inv H. rewrite Z.add_0_r. apply Ptrofs.unsigned_range_2.
 Qed.
 
 Let valid_different_pointers_inj:
@@ -1003,9 +1003,9 @@ Module NVal <: SEMILATTICE.
 
   Definition t := nval.
   Definition eq (x y: t) := (x = y).
-  Definition eq_refl: forall x, eq x x := (@refl_equal t).
-  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
-  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
+  Definition eq_refl: forall x, eq x x := (@eq_refl t).
+  Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t).
+  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t).
   Definition beq (x y: t) : bool := proj_sumbool (eq_nval x y).
   Lemma beq_correct: forall x y, beq x y = true -> eq x y.
   Proof. unfold beq; intros. InvBooleans. auto. Qed.
diff --git a/backend/RTL.v b/backend/RTL.v
index d191918c..16723d96 100644
--- a/backend/RTL.v
+++ b/backend/RTL.v
@@ -437,7 +437,7 @@ Definition instr_defs (i: instruction) : option reg :=
   the CFG of [f] are between 1 and [max_pc_function f] (inclusive). *)
 
 Definition max_pc_function (f: function) :=
-  PTree.fold (fun m pc i => Pmax m pc) f.(fn_code) 1%positive.
+  PTree.fold (fun m pc i => Pos.max m pc) f.(fn_code) 1%positive.
 
 Lemma max_pc_function_sound:
   forall f pc i, f.(fn_code)!pc = Some i -> Ple pc (max_pc_function f).
@@ -461,32 +461,32 @@ Qed.
 Definition max_reg_instr (m: positive) (pc: node) (i: instruction) :=
   match i with
   | Inop s => m
-  | Iop op args res s => fold_left Pmax args (Pmax res m)
-  | Iload chunk addr args dst s => fold_left Pmax args (Pmax dst m)
-  | Istore chunk addr args src s => fold_left Pmax args (Pmax src m)
-  | Icall sig (inl r) args res s => fold_left Pmax args (Pmax r (Pmax res m))
-  | Icall sig (inr id) args res s => fold_left Pmax args (Pmax res m)
-  | Itailcall sig (inl r) args => fold_left Pmax args (Pmax r m)
-  | Itailcall sig (inr id) args => fold_left Pmax args m
+  | Iop op args res s => fold_left Pos.max args (Pos.max res m)
+  | Iload chunk addr args dst s => fold_left Pos.max args (Pos.max dst m)
+  | Istore chunk addr args src s => fold_left Pos.max args (Pos.max src m)
+  | Icall sig (inl r) args res s => fold_left Pos.max args (Pos.max r (Pos.max res m))
+  | Icall sig (inr id) args res s => fold_left Pos.max args (Pos.max res m)
+  | Itailcall sig (inl r) args => fold_left Pos.max args (Pos.max r m)
+  | Itailcall sig (inr id) args => fold_left Pos.max args m
   | Ibuiltin ef args res s =>
-      fold_left Pmax (params_of_builtin_args args)
-        (fold_left Pmax (params_of_builtin_res res) m)
-  | Icond cond args ifso ifnot => fold_left Pmax args m
-  | Ijumptable arg tbl => Pmax arg m
+      fold_left Pos.max (params_of_builtin_args args)
+        (fold_left Pos.max (params_of_builtin_res res) m)
+  | Icond cond args ifso ifnot => fold_left Pos.max args m
+  | Ijumptable arg tbl => Pos.max arg m
   | Ireturn None => m
-  | Ireturn (Some arg) => Pmax arg m
+  | Ireturn (Some arg) => Pos.max arg m
   end.
 
 Definition max_reg_function (f: function) :=
-  Pmax
+  Pos.max
     (PTree.fold max_reg_instr f.(fn_code) 1%positive)
-    (fold_left Pmax f.(fn_params) 1%positive).
+    (fold_left Pos.max f.(fn_params) 1%positive).
 
 Remark max_reg_instr_ge:
   forall m pc i, Ple m (max_reg_instr m pc i).
 Proof.
   intros.
-  assert (X: forall l n, Ple m n -> Ple m (fold_left Pmax l n)).
+  assert (X: forall l n, Ple m n -> Ple m (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     auto.
     apply IHl. xomega. }
@@ -498,7 +498,7 @@ Remark max_reg_instr_def:
   forall m pc i r, instr_defs i = Some r -> Ple r (max_reg_instr m pc i).
 Proof.
   intros.
-  assert (X: forall l n, Ple r n -> Ple r (fold_left Pmax l n)).
+  assert (X: forall l n, Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros. xomega. apply IHl. xomega. }
   destruct i; simpl in *; inv H.
 - apply X. xomega.
@@ -511,7 +511,7 @@ Remark max_reg_instr_uses:
   forall m pc i r, In r (instr_uses i) -> Ple r (max_reg_instr m pc i).
 Proof.
   intros.
-  assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)).
+  assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     tauto.
     apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
@@ -564,11 +564,11 @@ Lemma max_reg_function_params:
   forall f r, In r f.(fn_params) -> Ple r (max_reg_function f).
 Proof.
   intros.
-  assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pmax l n)).
+  assert (X: forall l n, In r l \/ Ple r n -> Ple r (fold_left Pos.max l n)).
   { induction l; simpl; intros.
     tauto.
     apply IHl. destruct H0 as [[A|A]|A]. right; subst; xomega. auto. right; xomega. }
-  assert (Y: Ple r (fold_left Pmax f.(fn_params) 1%positive)).
+  assert (Y: Ple r (fold_left Pos.max f.(fn_params) 1%positive)).
   { apply X; auto. }
   unfold max_reg_function. xomega.
 Qed.
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 6d81f84b..9d7a8506 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -161,7 +161,7 @@ Definition init_state : state :=
 Remark add_instr_wf:
   forall s i pc,
   let n := s.(st_nextnode) in
-  Plt pc (Psucc n) \/ (PTree.set n i s.(st_code))!pc = None.
+  Plt pc (Pos.succ n) \/ (PTree.set n i s.(st_code))!pc = None.
 Proof.
   intros. case (peq pc n); intro.
   subst pc; left; apply Plt_succ.
@@ -175,7 +175,7 @@ Remark add_instr_incr:
   forall s i,
   let n := s.(st_nextnode) in
   state_incr s (mkstate s.(st_nextreg)
-                (Psucc n)
+                (Pos.succ n)
                 (PTree.set n i s.(st_code))
                 (add_instr_wf s i)).
 Proof.
@@ -189,7 +189,7 @@ Definition add_instr (i: instruction) : mon node :=
   fun s =>
     let n := s.(st_nextnode) in
     OK n
-       (mkstate s.(st_nextreg) (Psucc n) (PTree.set n i s.(st_code))
+       (mkstate s.(st_nextreg) (Pos.succ n) (PTree.set n i s.(st_code))
                 (add_instr_wf s i))
        (add_instr_incr s i).
 
@@ -199,7 +199,7 @@ Definition add_instr (i: instruction) : mon node :=
 
 Remark reserve_instr_wf:
   forall s pc,
-  Plt pc (Psucc s.(st_nextnode)) \/ s.(st_code)!pc = None.
+  Plt pc (Pos.succ s.(st_nextnode)) \/ s.(st_code)!pc = None.
 Proof.
   intros. elim (st_wf s pc); intro.
   left; apply Plt_trans_succ; auto.
@@ -210,7 +210,7 @@ Remark reserve_instr_incr:
   forall s,
   let n := s.(st_nextnode) in
   state_incr s (mkstate s.(st_nextreg)
-                (Psucc n)
+                (Pos.succ n)
                 s.(st_code)
                 (reserve_instr_wf s)).
 Proof.
@@ -224,7 +224,7 @@ Definition reserve_instr: mon node :=
   fun (s: state) =>
   let n := s.(st_nextnode) in
   OK n
-     (mkstate s.(st_nextreg) (Psucc n) s.(st_code) (reserve_instr_wf s))
+     (mkstate s.(st_nextreg) (Pos.succ n) s.(st_code) (reserve_instr_wf s))
      (reserve_instr_incr s).
 
 Remark update_instr_wf:
@@ -275,7 +275,7 @@ Definition update_instr (n: node) (i: instruction) : mon unit :=
 
 Remark new_reg_incr:
   forall s,
-  state_incr s (mkstate (Psucc s.(st_nextreg))
+  state_incr s (mkstate (Pos.succ s.(st_nextreg))
                         s.(st_nextnode) s.(st_code) s.(st_wf)).
 Proof.
   constructor; simpl. apply Ple_refl. apply Ple_succ. auto.
@@ -284,7 +284,7 @@ Qed.
 Definition new_reg : mon reg :=
   fun s =>
     OK s.(st_nextreg)
-       (mkstate (Psucc s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf))
+       (mkstate (Pos.succ s.(st_nextreg)) s.(st_nextnode) s.(st_code) s.(st_wf))
        (new_reg_incr s).
 
 (** ** Operations on mappings *)
@@ -651,7 +651,7 @@ Definition alloc_label (lbl: Cminor.label) (maps: labelmap * state) : labelmap *
   let (map, s) := maps in
   let n := s.(st_nextnode) in
   (PTree.set lbl n map,
-   mkstate s.(st_nextreg) (Psucc s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)).
+   mkstate s.(st_nextreg) (Pos.succ s.(st_nextnode)) s.(st_code) (reserve_instr_wf s)).
 
 Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
                         {struct s} : labelmap * state :=
diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v
index 93f209b7..072db138 100644
--- a/backend/RTLgenproof.v
+++ b/backend/RTLgenproof.v
@@ -301,7 +301,7 @@ Proof.
   destruct (map_letvars x0). auto. simpl in me_letvars0. inversion me_letvars0.
   intros. rewrite Regmap.gso. apply UNDEF.
   apply reg_fresh_decr with s2; eauto with rtlg.
-  apply sym_not_equal. apply valid_fresh_different with s2; auto.
+  apply not_eq_sym. apply valid_fresh_different with s2; auto.
 Qed.
 
 Lemma match_set_locals:
@@ -1535,7 +1535,7 @@ Proof.
     assert (map_valid init_mapping s0) by apply init_mapping_valid.
     exploit (add_vars_valid (CminorSel.fn_params f)); eauto. intros [A B].
     eapply add_vars_wf; eauto. eapply add_vars_wf; eauto. apply init_mapping_wf.
-  edestruct Mem.alloc_extends as [tm' []]; eauto; try apply Zle_refl.
+  edestruct Mem.alloc_extends as [tm' []]; eauto; try apply Z.le_refl.
   econstructor; split.
   left; apply plus_one. eapply exec_function_internal; simpl; eauto.
   simpl. econstructor; eauto.
diff --git a/backend/SelectDivproof.v b/backend/SelectDivproof.v
index fe5bfe28..75713289 100644
--- a/backend/SelectDivproof.v
+++ b/backend/SelectDivproof.v
@@ -36,7 +36,7 @@ Lemma Zdiv_mul_pos:
   two_p (N+l) <= m * d <= two_p (N+l) + two_p l ->
   forall n,
   0 <= n < two_p N ->
-  Zdiv n d = Zdiv (m * n) (two_p (N + l)).
+  Z.div n d = Z.div (m * n) (two_p (N + l)).
 Proof.
   intros m l l_pos [LO HI] n RANGE.
   exploit (Z_div_mod_eq n d). auto.
@@ -54,9 +54,9 @@ Proof.
   assert ((m * n - two_p (N + l) * q) * d = k * n + two_p (N + l) * r).
     unfold k. rewrite EUCL. ring.
   assert (0 <= k * n).
-    apply Zmult_le_0_compat; omega.
+    apply Z.mul_nonneg_nonneg; omega.
   assert (k * n <= two_p (N + l) - two_p l).
-    apply Zle_trans with (two_p l * n).
+    apply Z.le_trans with (two_p l * n).
     apply Zmult_le_compat_r. omega. omega.
     replace (N + l) with (l + N) by omega.
     rewrite two_p_is_exp.
@@ -66,7 +66,7 @@ Proof.
     apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
     omega. omega.
   assert (0 <= two_p (N + l) * r).
-    apply Zmult_le_0_compat.
+    apply Z.mul_nonneg_nonneg.
     exploit (two_p_gt_ZERO (N + l)). omega. omega.
     omega.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
@@ -81,7 +81,7 @@ Proof.
   assert (m * n - two_p (N + l) * q < two_p (N + l)).
     apply Zmult_lt_reg_r with d. omega.
     rewrite H2.
-    apply Zle_lt_trans with (two_p (N + l) * d - two_p l).
+    apply Z.le_lt_trans with (two_p (N + l) * d - two_p l).
     omega.
     exploit (two_p_gt_ZERO l). omega. omega.
   symmetry. apply Zdiv_unique with (m * n - two_p (N + l) * q).
@@ -89,7 +89,7 @@ Proof.
 Qed.
 
 Lemma Zdiv_unique_2:
-  forall x y q, y > 0 -> 0 < y * q - x <= y -> Zdiv x y = q - 1.
+  forall x y q, y > 0 -> 0 < y * q - x <= y -> Z.div x y = q - 1.
 Proof.
   intros. apply Zdiv_unique with (x - (q - 1) * y). ring.
   replace ((q - 1) * y) with (y * q - y) by ring. omega.
@@ -101,7 +101,7 @@ Lemma Zdiv_mul_opp:
   two_p (N+l) < m * d <= two_p (N+l) + two_p l ->
   forall n,
   0 < n <= two_p N ->
-  Zdiv n d = - Zdiv (m * (-n)) (two_p (N + l)) - 1.
+  Z.div n d = - Z.div (m * (-n)) (two_p (N + l)) - 1.
 Proof.
   intros m l l_pos [LO HI] n RANGE.
   replace (m * (-n)) with (- (m * n)) by ring.
@@ -114,7 +114,7 @@ Proof.
   assert (0 <= m).
     apply Zmult_le_0_reg_r with d. auto.
     exploit (two_p_gt_ZERO (N + l)). omega. omega.
-  cut (Zdiv (- (m * n)) (two_p (N + l)) = -q - 1).
+  cut (Z.div (- (m * n)) (two_p (N + l)) = -q - 1).
     omega.
   apply Zdiv_unique_2.
   apply two_p_gt_ZERO. omega.
@@ -130,15 +130,15 @@ Proof.
   apply Zmult_lt_reg_r with d. omega.
   replace (0 * d) with 0 by omega.
   rewrite H2.
-  assert (0 < k * n). apply Zmult_lt_0_compat; omega.
+  assert (0 < k * n). apply Z.mul_pos_pos; omega.
   assert (0 <= two_p (N + l) * r).
-    apply Zmult_le_0_compat. exploit (two_p_gt_ZERO (N + l)); omega. omega.
+    apply Z.mul_nonneg_nonneg. exploit (two_p_gt_ZERO (N + l)); omega. omega.
   omega.
   apply Zmult_le_reg_r with d. omega.
   rewrite H2.
   assert (k * n <= two_p (N + l)).
-    rewrite Zplus_comm. rewrite two_p_is_exp; try omega.
-    apply Zle_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega.
+    rewrite Z.add_comm. rewrite two_p_is_exp; try omega.
+    apply Z.le_trans with (two_p l * n). apply Zmult_le_compat_r. omega. omega.
     apply Zmult_le_compat_l. omega. exploit (two_p_gt_ZERO l). omega. omega.
   assert (two_p (N + l) * r <= two_p (N + l) * d - two_p (N + l)).
     replace (two_p (N + l) * d - two_p (N + l))
@@ -156,7 +156,7 @@ Lemma Zquot_mul:
   two_p (N+l) < m * d <= two_p (N+l) + two_p l ->
   forall n,
   - two_p N <= n < two_p N ->
-  Z.quot n d = Zdiv (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0).
+  Z.quot n d = Z.div (m * n) (two_p (N + l)) + (if zlt n 0 then 1 else 0).
 Proof.
   intros. destruct (zlt n 0).
   exploit (Zdiv_mul_opp m l H H0 (-n)). omega.
@@ -164,7 +164,7 @@ Proof.
   replace (Z.quot n d) with (- Z.quot (-n) d).
   rewrite Zquot_Zdiv_pos by omega. omega.
   rewrite Z.quot_opp_l by omega. ring.
-  rewrite Zplus_0_r. rewrite Zquot_Zdiv_pos by omega.
+  rewrite Z.add_0_r. rewrite Zquot_Zdiv_pos by omega.
   apply Zdiv_mul_pos; omega.
 Qed.
 
@@ -178,7 +178,7 @@ Lemma divs_mul_params_sound:
   0 <= m < Int.modulus /\ 0 <= p < 32 /\
   forall n,
   Int.min_signed <= n <= Int.max_signed ->
-  Z.quot n d = Zdiv (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0).
+  Z.quot n d = Z.div (m * n) (two_p (32 + p)) + (if zlt n 0 then 1 else 0).
 Proof with (try discriminate).
   unfold divs_mul_params; intros d m' p'.
   destruct (find_div_mul_params Int.wordsize
@@ -207,7 +207,7 @@ Lemma divu_mul_params_sound:
   0 <= m < Int.modulus /\ 0 <= p < 32 /\
   forall n,
   0 <= n < Int.modulus ->
-  Zdiv n d = Zdiv (m * n) (two_p (32 + p)).
+  Z.div n d = Z.div (m * n) (two_p (32 + p)).
 Proof with (try discriminate).
   unfold divu_mul_params; intros d m' p'.
   destruct (find_div_mul_params Int.wordsize
@@ -246,9 +246,9 @@ Proof.
   unfold Int.max_signed; omega.
   apply Zdiv_interval_1. generalize Int.min_signed_neg; omega. apply Int.half_modulus_pos.
   apply Int.modulus_pos.
-  split. apply Zle_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega.
+  split. apply Z.le_trans with (Int.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int.min_signed_neg; omega.
   apply Zmult_le_compat_r. unfold n; generalize (Int.signed_range x); tauto. tauto.
-  apply Zle_lt_trans with (Int.half_modulus * m).
+  apply Z.le_lt_trans with (Int.half_modulus * m).
   apply Zmult_le_compat_r. generalize (Int.signed_range x); unfold n, Int.max_signed; omega. tauto.
   apply Zmult_lt_compat_l. generalize Int.half_modulus_pos; omega. tauto.
   assert (32 < Int.max_unsigned) by (compute; auto). omega.
@@ -310,7 +310,7 @@ Proof.
   unfold Int.max_unsigned; omega.
   apply Zdiv_interval_1. omega. compute; auto. compute; auto.
   split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int.unsigned_range x); omega. omega.
-  apply Zle_lt_trans with (Int.modulus * m).
+  apply Z.le_lt_trans with (Int.modulus * m).
   apply Zmult_le_compat_r. generalize (Int.unsigned_range x); omega. omega.
   apply Zmult_lt_compat_l. compute; auto. omega.
   unfold Int.max_unsigned; omega.
@@ -325,7 +325,7 @@ Lemma divls_mul_params_sound:
   0 <= m < Int64.modulus /\ 0 <= p < 64 /\
   forall n,
   Int64.min_signed <= n <= Int64.max_signed ->
-  Z.quot n d = Zdiv (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0).
+  Z.quot n d = Z.div (m * n) (two_p (64 + p)) + (if zlt n 0 then 1 else 0).
 Proof with (try discriminate).
   unfold divls_mul_params; intros d m' p'.
   destruct (find_div_mul_params Int64.wordsize
@@ -354,7 +354,7 @@ Lemma divlu_mul_params_sound:
   0 <= m < Int64.modulus /\ 0 <= p < 64 /\
   forall n,
   0 <= n < Int64.modulus ->
-  Zdiv n d = Zdiv (m * n) (two_p (64 + p)).
+  Z.div n d = Z.div (m * n) (two_p (64 + p)).
 Proof with (try discriminate).
   unfold divlu_mul_params; intros d m' p'.
   destruct (find_div_mul_params Int64.wordsize
@@ -399,9 +399,9 @@ Proof.
   unfold Int64.max_signed; omega.
   apply Zdiv_interval_1. generalize Int64.min_signed_neg; omega. apply Int64.half_modulus_pos.
   apply Int64.modulus_pos.
-  split. apply Zle_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega.
+  split. apply Z.le_trans with (Int64.min_signed * m). apply Zmult_le_compat_l_neg. omega. generalize Int64.min_signed_neg; omega.
   apply Zmult_le_compat_r. unfold n; generalize (Int64.signed_range x); tauto. tauto.
-  apply Zle_lt_trans with (Int64.half_modulus * m).
+  apply Z.le_lt_trans with (Int64.half_modulus * m).
   apply Zmult_le_compat_r. generalize (Int64.signed_range x); unfold n, Int64.max_signed; omega. tauto.
   apply Zmult_lt_compat_l. generalize Int64.half_modulus_pos; omega. tauto.
   assert (64 < Int.max_unsigned) by (compute; auto). omega.
@@ -469,7 +469,7 @@ Proof.
   unfold Int64.max_unsigned; omega.
   apply Zdiv_interval_1. omega. compute; auto. compute; auto.
   split. simpl. apply Z.mul_nonneg_nonneg. generalize (Int64.unsigned_range x); omega. omega.
-  apply Zle_lt_trans with (Int64.modulus * m).
+  apply Z.le_lt_trans with (Int64.modulus * m).
   apply Zmult_le_compat_r. generalize (Int64.unsigned_range x); omega. omega.
   apply Zmult_lt_compat_l. compute; auto. omega.
   unfold Int64.max_unsigned; omega.
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v
index ebc64c6f..86d7ff21 100644
--- a/backend/Selectionproof.v
+++ b/backend/Selectionproof.v
@@ -209,7 +209,7 @@ Lemma eval_load:
 Proof.
   intros. generalize H0; destruct v; simpl; intro; try discriminate.
   unfold load.
-  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)).
+  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)).
   destruct (addressing chunk a). intros [vl [EV EQ]].
   eapply eval_Eload; eauto.
 Qed.
@@ -224,7 +224,7 @@ Lemma eval_store:
 Proof.
   intros. generalize H1; destruct v1; simpl; intro; try discriminate.
   unfold store.
-  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)).
+  generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (eq_refl _)).
   destruct (addressing chunk a1). intros [vl [EV EQ]].
   eapply step_store; eauto.
 Qed.
@@ -1036,7 +1036,7 @@ Proof.
 - (* internal function *)
   destruct TF as (hf & HF & TF). specialize (MC cunit hf).
   monadInv TF. generalize EQ; intros TF; monadInv TF.
-  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl.
+  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros [m2' [A B]].
   left; econstructor; split.
   econstructor; simpl; eauto.
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v
index d3d901b6..f7570f57 100644
--- a/backend/Stackingproof.v
+++ b/backend/Stackingproof.v
@@ -133,7 +133,7 @@ Qed.
 Remark bound_stack_data_stacksize:
   f.(Linear.fn_stacksize) <= b.(bound_stack_data).
 Proof.
-  unfold b, function_bounds, bound_stack_data. apply Zmax1.
+  unfold b, function_bounds, bound_stack_data. apply Z.le_max_l.
 Qed.
 
 (** * Memory assertions used to describe the contents of stack frames *)
@@ -217,7 +217,7 @@ Proof.
 - red; intros. apply Mem.perm_implies with Freeable; auto with mem.
   apply H0. rewrite size_type_chunk, typesize_typesize in H4. omega.
 - rewrite align_type_chunk. apply Z.divide_add_r.
-  apply Zdivide_trans with 8; auto.
+  apply Z.divide_trans with 8; auto.
   exists (8 / (4 * typealign ty)); destruct ty; reflexivity.
   apply Z.mul_divide_mono_l. auto.
 Qed.
@@ -962,7 +962,7 @@ Local Opaque mreg_type.
   assert (SZREC: pos1 + sz <= size_callee_save_area_rec l (pos1 + sz)) by (apply size_callee_save_area_rec_incr).
   assert (POS1: pos <= pos1) by (apply align_le; auto).
   assert (AL1: (align_chunk (chunk_of_type ty) | pos1)).
-  { unfold pos1. apply Zdivide_trans with sz.
+  { unfold pos1. apply Z.divide_trans with sz.
     unfold sz; rewrite <- size_type_chunk. apply align_size_chunk_divides.
     apply align_divides; auto. }
   apply range_drop_left with (mid := pos1) in SEP; [ | omega ].
@@ -1984,7 +1984,7 @@ Proof.
   econstructor; eauto with coqlib.
   apply Val.Vptr_has_type.
   intros; red.
-    apply Zle_trans with (size_arguments (Linear.funsig f')); auto.
+    apply Z.le_trans with (size_arguments (Linear.funsig f')); auto.
     apply loc_arguments_bounded; auto.
   simpl; red; auto.
   simpl. rewrite sep_assoc. exact SEP.
diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v
index 6acf2bbd..c6644ceb 100644
--- a/backend/Tunnelingproof.v
+++ b/backend/Tunnelingproof.v
@@ -505,7 +505,7 @@ Proof.
   eapply exec_Lreturn; eauto.
   constructor; eauto using return_regs_lessdef, match_parent_locset.
 - (* internal function *)
-  exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. 
+  exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros (tm' & ALLOC & MEM'). 
   left; simpl; econstructor; split.
   eapply exec_function_internal; eauto.
diff --git a/backend/Unusedglobproof.v b/backend/Unusedglobproof.v
index 446ffb7f..7899a04c 100644
--- a/backend/Unusedglobproof.v
+++ b/backend/Unusedglobproof.v
@@ -835,7 +835,7 @@ Proof.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
 - econstructor; eauto with barg.
-- simpl in H. exploit Mem.load_inject; eauto. rewrite Zplus_0_r.
+- simpl in H. exploit Mem.load_inject; eauto. rewrite Z.add_0_r.
   intros (v' & A & B). exists v'; auto with barg.
 - econstructor; split; eauto with barg. simpl. econstructor; eauto. rewrite Ptrofs.add_zero; auto.
 - assert (Val.inject j (Senv.symbol_address ge id ofs) (Senv.symbol_address tge id ofs)).
@@ -956,7 +956,7 @@ Proof.
   eapply match_stacks_preserves_globals; eauto. eauto.
   destruct ros as [r|id]. eauto. apply KEPT. red. econstructor; econstructor; split; eauto. simpl; auto.
   intros (A & B).
-  exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D).
+  exploit Mem.free_parallel_inject; eauto. rewrite ! Z.add_0_r. intros (tm' & C & D).
   econstructor; split.
   eapply exec_Itailcall; eauto.
   econstructor; eauto.
@@ -999,7 +999,7 @@ Proof.
   econstructor; eauto.
 
 - (* return *)
-  exploit Mem.free_parallel_inject; eauto. rewrite ! Zplus_0_r. intros (tm' & C & D).
+  exploit Mem.free_parallel_inject; eauto. rewrite ! Z.add_0_r. intros (tm' & C & D).
   econstructor; split.
   eapply exec_Ireturn; eauto.
   econstructor; eauto.
@@ -1011,7 +1011,7 @@ Proof.
   destruct or; simpl; auto.
 
 - (* internal function *)
-  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Zle_refl. apply Zle_refl.
+  exploit Mem.alloc_parallel_inject. eauto. eauto. apply Z.le_refl. apply Z.le_refl.
   intros (j' & tm' & tstk & C & D & E & F & G).
   assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto).
   assert (TSTK: tstk = Mem.nextblock tm) by (eapply Mem.alloc_result; eauto).
@@ -1124,7 +1124,7 @@ Lemma Mem_getN_forall2:
 Proof.
   induction n; simpl Mem.getN; intros.
 - simpl in H1. omegaContradiction.
-- inv H. rewrite inj_S in H1. destruct (zeq i p0).
+- inv H. rewrite Nat2Z.inj_succ in H1. destruct (zeq i p0).
 + congruence.
 + apply IHn with (p0 + 1); auto. omega. omega.
 Qed.
@@ -1145,7 +1145,7 @@ Proof.
   apply Mem.perm_cur. eapply Mem.perm_implies; eauto.
   apply P2. omega.
 - exploit init_meminj_invert; eauto. intros (A & id & B & C).
-  subst delta. apply Zdivide_0.
+  subst delta. apply Z.divide_0_r.
 - exploit init_meminj_invert_strong; eauto. intros (A & id & gd & B & C & D & E & F).
   exploit (Genv.init_mem_characterization_gen p); eauto.
   exploit (Genv.init_mem_characterization_gen tp); eauto.
@@ -1159,7 +1159,7 @@ Proof.
 Local Transparent Mem.loadbytes.
   generalize (S1 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E1; inv E1.
   generalize (S2 NO). unfold Mem.loadbytes. destruct Mem.range_perm_dec; intros E2; inv E2.
-  rewrite Zplus_0_r.
+  rewrite Z.add_0_r.
   apply Mem_getN_forall2 with (p := 0) (n := nat_of_Z (init_data_list_size (gvar_init v))).
   rewrite H3, H4. apply bytes_of_init_inject. auto.
   omega.
diff --git a/backend/ValueAnalysis.v b/backend/ValueAnalysis.v
index 7c4c0525..8aa4878a 100644
--- a/backend/ValueAnalysis.v
+++ b/backend/ValueAnalysis.v
@@ -875,7 +875,7 @@ Proof.
     apply smatch_ge with Nonstack. eapply SM. eapply mmatch_top; eauto. apply pge_lub_r.
   + (* below *)
     red; simpl; intros. destruct (eq_block b sp).
-    subst b. apply Plt_le_trans with bound. apply BELOW. congruence. auto.
+    subst b. apply Pos.lt_le_trans with bound. apply BELOW. congruence. auto.
     eapply mmatch_below; eauto.
 - (* genv *)
   eapply genv_match_exten; eauto.
@@ -1008,7 +1008,7 @@ Proof.
   + apply SMTOP; auto.
   + apply SMTOP; auto.
   + red; simpl; intros. destruct (plt b (Mem.nextblock m)).
-    eapply Plt_le_trans. eauto. eapply external_call_nextblock; eauto.
+    eapply Pos.lt_le_trans. eauto. eapply external_call_nextblock; eauto.
     destruct (j' b) as [[bx deltax] | ] eqn:J'.
     eapply Mem.valid_block_inject_1; eauto.
     congruence.
diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v
index f905ffa2..d7eaa228 100644
--- a/backend/ValueDomain.v
+++ b/backend/ValueDomain.v
@@ -750,7 +750,7 @@ Definition sgn (p: aptr) (n: Z) : aval :=
   if zle n 8 then Sgn p 8 else if zle n 16 then Sgn p 16 else Ifptr p.
 
 Lemma vmatch_uns':
-  forall p i n, is_uns (Zmax 0 n) i -> vmatch (Vint i) (uns p n).
+  forall p i n, is_uns (Z.max 0 n) i -> vmatch (Vint i) (uns p n).
 Proof.
   intros.
   assert (A: forall n', n' >= 0 -> n' >= n -> is_uns n' i) by (eauto with va).
@@ -780,7 +780,7 @@ Proof.
 Qed.
 
 Lemma vmatch_sgn':
-  forall p i n, is_sgn (Zmax 1 n) i -> vmatch (Vint i) (sgn p n).
+  forall p i n, is_sgn (Z.max 1 n) i -> vmatch (Vint i) (sgn p n).
 Proof.
   intros.
   assert (A: forall n', n' >= 1 -> n' >= n -> is_sgn n' i) by (eauto with va).
@@ -3476,7 +3476,7 @@ Lemma ablock_storebytes_contents:
   forall ab p i sz j chunk' av',
   (ablock_storebytes ab p i sz).(ab_contents)##j = Some(ACval chunk' av') ->
   ab.(ab_contents)##j = Some (ACval chunk' av')
-  /\ (j + size_chunk chunk' <= i \/ i + Zmax sz 0 <= j).
+  /\ (j + size_chunk chunk' <= i \/ i + Z.max sz 0 <= j).
 Proof.
   unfold ablock_storebytes; simpl; intros.
   exploit inval_before_contents; eauto. clear H. intros [A B].
@@ -4284,13 +4284,13 @@ Proof.
   intros. constructor. constructor.
 - (* perms *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
-  rewrite Zplus_0_r. auto.
+  rewrite Z.add_0_r. auto.
 - (* alignment *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
-  apply Zdivide_0.
+  apply Z.divide_0_r.
 - (* contents *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
-  rewrite Zplus_0_r.
+  rewrite Z.add_0_r.
   set (mv := ZMap.get ofs (PMap.get b1 (Mem.mem_contents m))).
   assert (Mem.loadbytes m b1 ofs 1 = Some (mv :: nil)).
   {
@@ -4317,10 +4317,10 @@ Proof.
   auto.
 - (* overflow *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
-  rewrite Zplus_0_r. split. omega. apply Ptrofs.unsigned_range_2.
+  rewrite Z.add_0_r. split. omega. apply Ptrofs.unsigned_range_2.
 - (* perm inv *)
   intros. exploit inj_of_bc_inv; eauto. intros (A & B & C); subst.
-  rewrite Zplus_0_r in H2. auto.
+  rewrite Z.add_0_r in H2. auto.
 Qed.
 
 Lemma inj_of_bc_preserves_globals:
@@ -4371,9 +4371,9 @@ Module AVal <: SEMILATTICE_WITH_TOP.
 
   Definition t := aval.
   Definition eq (x y: t) := (x = y).
-  Definition eq_refl: forall x, eq x x := (@refl_equal t).
-  Definition eq_sym: forall x y, eq x y -> eq y x := (@sym_equal t).
-  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@trans_equal t).
+  Definition eq_refl: forall x, eq x x := (@eq_refl t).
+  Definition eq_sym: forall x y, eq x y -> eq y x := (@eq_sym t).
+  Definition eq_trans: forall x y z, eq x y -> eq y z -> eq x z := (@eq_trans t).
   Definition beq (x y: t) : bool := proj_sumbool (eq_aval x y).
   Lemma beq_correct: forall x y, beq x y = true -> eq x y.
   Proof. unfold beq; intros. InvBooleans. auto. Qed.
-- 
cgit