Remove coq warnings (#28)

Replace deprecated functions and theorems from the Coq standard library (version 8.6) by their non-deprecated counterparts.

11 files changed, 182 insertions, 182 deletions

diff --git a/lib/Coqlib.v b/lib/Coqlib.v
index 18d4d7e1..3fe1ea2e 100644
--- a/lib/Coqlib.v
+++ b/lib/Coqlib.v
@@ -32,7 +32,7 @@ Ltac predSpec pred predspec x y :=
   generalize (predspec x y); case (pred x y); intro.
 
 Ltac caseEq name :=
-  generalize (refl_equal name); pattern name at -1 in |- *; case name.
+  generalize (eq_refl name); pattern name at -1 in |- *; case name.
 
 Ltac destructEq name :=
   destruct name eqn:?.
@@ -125,21 +125,21 @@ Lemma Plt_trans:
 Proof (Pos.lt_trans).
 
 Lemma Plt_succ:
-  forall (x: positive), Plt x (Psucc x).
+  forall (x: positive), Plt x (Pos.succ x).
 Proof.
   unfold Plt; intros. apply Pos.lt_succ_r. apply Pos.le_refl.
 Qed.
 Hint Resolve Plt_succ: coqlib.
 
 Lemma Plt_trans_succ:
-  forall (x y: positive), Plt x y -> Plt x (Psucc y).
+  forall (x y: positive), Plt x y -> Plt x (Pos.succ y).
 Proof.
   intros. apply Plt_trans with y. assumption. apply Plt_succ.
 Qed.
 Hint Resolve Plt_succ: coqlib.
 
 Lemma Plt_succ_inv:
-  forall (x y: positive), Plt x (Psucc y) -> Plt x y \/ x = y.
+  forall (x y: positive), Plt x (Pos.succ y) -> Plt x y \/ x = y.
 Proof.
   unfold Plt; intros. rewrite Pos.lt_succ_r in H.
   apply Pos.le_lteq; auto.
@@ -165,7 +165,7 @@ Proof (Pos.le_trans).
 Lemma Plt_Ple: forall (p q: positive), Plt p q -> Ple p q.
 Proof (Pos.lt_le_incl).
 
-Lemma Ple_succ: forall (p: positive), Ple p (Psucc p).
+Lemma Ple_succ: forall (p: positive), Ple p (Pos.succ p).
 Proof.
   intros. apply Plt_Ple. apply Plt_succ.
 Qed.
@@ -188,7 +188,7 @@ Section POSITIVE_ITERATION.
 
 Lemma Plt_wf: well_founded Plt.
 Proof.
-  apply well_founded_lt_compat with nat_of_P.
+  apply well_founded_lt_compat with Pos.to_nat.
   intros. apply nat_of_P_lt_Lt_compare_morphism. exact H.
 Qed.
 
@@ -197,16 +197,16 @@ Variable v1: A.
 Variable f: positive -> A -> A.
 
 Lemma Ppred_Plt:
-  forall x, x <> xH -> Plt (Ppred x) x.
+  forall x, x <> xH -> Plt (Pos.pred x) x.
 Proof.
-  intros. elim (Psucc_pred x); intro. contradiction.
-  set (y := Ppred x) in *. rewrite <- H0. apply Plt_succ.
+  intros. elim (Pos.succ_pred_or x); intro. contradiction.
+  set (y := Pos.pred x) in *. rewrite <- H0. apply Plt_succ.
 Qed.
 
 Let iter (x: positive) (P: forall y, Plt y x -> A) : A :=
   match peq x xH with
   | left EQ => v1
-  | right NOTEQ => f (Ppred x) (P (Ppred x) (Ppred_Plt x NOTEQ))
+  | right NOTEQ => f (Pos.pred x) (P (Pos.pred x) (Ppred_Plt x NOTEQ))
   end.
 
 Definition positive_rec : positive -> A :=
@@ -228,18 +228,18 @@ Proof.
 Qed.
 
 Lemma positive_rec_succ:
-  forall x, positive_rec (Psucc x) = f x (positive_rec x).
+  forall x, positive_rec (Pos.succ x) = f x (positive_rec x).
 Proof.
   intro. rewrite unroll_positive_rec. unfold iter.
-  case (peq (Psucc x) 1); intro.
+  case (peq (Pos.succ x) 1); intro.
   destruct x; simpl in e; discriminate.
-  rewrite Ppred_succ. auto.
+  rewrite Pos.pred_succ. auto.
 Qed.
 
 Lemma positive_Peano_ind:
   forall (P: positive -> Prop),
   P xH ->
-  (forall x, P x -> P (Psucc x)) ->
+  (forall x, P x -> P (Pos.succ x)) ->
   forall x, P x.
 Proof.
   intros.
@@ -247,7 +247,7 @@ Proof.
   intros.
   case (peq x0 xH); intro.
   subst x0; auto.
-  elim (Psucc_pred x0); intro. contradiction. rewrite <- H2.
+  elim (Pos.succ_pred_or x0); intro. contradiction. rewrite <- H2.
   apply H0. apply H1. apply Ppred_Plt. auto.
 Qed.
 
@@ -327,10 +327,10 @@ Proof.
 Qed.
 
 Lemma two_power_nat_two_p:
-  forall x, two_power_nat x = two_p (Z_of_nat x).
+  forall x, two_power_nat x = two_p (Z.of_nat x).
 Proof.
   induction x. auto.
-  rewrite two_power_nat_S. rewrite inj_S. rewrite two_p_S. omega. omega.
+  rewrite two_power_nat_S. rewrite Nat2Z.inj_succ. rewrite two_p_S. omega. omega.
 Qed.
 
 Lemma two_p_monotone:
@@ -350,7 +350,7 @@ Lemma two_p_monotone_strict:
 Proof.
   intros. assert (two_p x <= two_p (y - 1)). apply two_p_monotone; omega.
   assert (two_p (y - 1) > 0). apply two_p_gt_ZERO. omega.
-  replace y with (Zsucc (y - 1)) by omega. rewrite two_p_S. omega. omega.
+  replace y with (Z.succ (y - 1)) by omega. rewrite two_p_S. omega. omega.
 Qed.
 
 Lemma two_p_strict:
@@ -375,37 +375,37 @@ Qed.
 (** Properties of [Zmin] and [Zmax] *)
 
 Lemma Zmin_spec:
-  forall x y, Zmin x y = if zlt x y then x else y.
+  forall x y, Z.min x y = if zlt x y then x else y.
 Proof.
-  intros. case (zlt x y); unfold Zlt, Zge; intro z.
-  unfold Zmin. rewrite z. auto.
-  unfold Zmin. caseEq (x ?= y); intro.
-  apply Zcompare_Eq_eq. auto.
+  intros. case (zlt x y); unfold Z.lt, Z.ge; intro z.
+  unfold Z.min. rewrite z. auto.
+  unfold Z.min. caseEq (x ?= y); intro.
+  apply Z.compare_eq. auto.
   contradiction.
   reflexivity.
 Qed.
 
 Lemma Zmax_spec:
-  forall x y, Zmax x y = if zlt y x then x else y.
+  forall x y, Z.max x y = if zlt y x then x else y.
 Proof.
-  intros. case (zlt y x); unfold Zlt, Zge; intro z.
-  unfold Zmax. rewrite <- (Zcompare_antisym y x).
+  intros. case (zlt y x); unfold Z.lt, Z.ge; intro z.
+  unfold Z.max. rewrite <- (Zcompare_antisym y x).
   rewrite z. simpl. auto.
-  unfold Zmax. rewrite <- (Zcompare_antisym y x).
+  unfold Z.max. rewrite <- (Zcompare_antisym y x).
   caseEq (y ?= x); intro; simpl.
-  symmetry. apply Zcompare_Eq_eq. auto.
+  symmetry. apply Z.compare_eq. auto.
   contradiction. reflexivity.
 Qed.
 
 Lemma Zmax_bound_l:
-  forall x y z, x <= y -> x <= Zmax y z.
+  forall x y z, x <= y -> x <= Z.max y z.
 Proof.
-  intros. generalize (Zmax1 y z). omega.
+  intros. generalize (Z.le_max_l y z). omega.
 Qed.
 Lemma Zmax_bound_r:
-  forall x y z, x <= z -> x <= Zmax y z.
+  forall x y z, x <= z -> x <= Z.max y z.
 Proof.
-  intros. generalize (Zmax2 y z). omega.
+  intros. generalize (Z.le_max_r y z). omega.
 Qed.
 
 (** Properties of Euclidean division and modulus. *)
@@ -444,7 +444,7 @@ Lemma Zmod_unique:
   forall x y a b,
   x = a * y + b -> 0 <= b < y -> x mod y = b.
 Proof.
-  intros. subst x. rewrite Zplus_comm.
+  intros. subst x. rewrite Z.add_comm.
   rewrite Z_mod_plus. apply Zmod_small. auto. omega.
 Qed.
 
@@ -452,7 +452,7 @@ Lemma Zdiv_unique:
   forall x y a b,
   x = a * y + b -> 0 <= b < y -> x / y = a.
 Proof.
-  intros. subst x. rewrite Zplus_comm.
+  intros. subst x. rewrite Z.add_comm.
   rewrite Z_div_plus. rewrite (Zdiv_small b y H0). omega. omega.
 Qed.
 
@@ -468,7 +468,7 @@ Proof.
   symmetry. apply Zdiv_unique with (r2 * b + r1).
   rewrite H2. rewrite H4. ring.
   split.
-  assert (0 <= r2 * b). apply Zmult_le_0_compat. omega. omega. omega.
+  assert (0 <= r2 * b). apply Z.mul_nonneg_nonneg. omega. omega. omega.
   assert ((r2 + 1) * b <= c * b).
   apply Zmult_le_compat_r. omega. omega.
   replace ((r2 + 1) * b) with (r2 * b + b) in H5 by ring.
@@ -498,7 +498,7 @@ Proof.
   split.
   assert (lo < (q + 1)).
   apply Zmult_lt_reg_r with b. omega.
-  apply Zle_lt_trans with a. omega.
+  apply Z.le_lt_trans with a. omega.
   replace ((q + 1) * b) with (b * q + b) by ring.
   omega.
   omega.
@@ -534,11 +534,11 @@ Proof.
   generalize (Z_div_mod_eq x b H0); fold xb; intro EQ1.
   generalize (Z_div_mod_eq xb a H); intro EQ2.
   rewrite EQ2 in EQ1.
-  eapply trans_eq. eexact EQ1. ring.
+  eapply eq_trans. eexact EQ1. ring.
   generalize (Z_mod_lt x b H0). intro.
   generalize (Z_mod_lt xb a H). intro.
   assert (0 <= xb mod a * b <= a * b - b).
-    split. apply Zmult_le_0_compat; omega.
+    split. apply Z.mul_nonneg_nonneg; omega.
     replace (a * b - b) with ((a - 1) * b) by ring.
     apply Zmult_le_compat; omega.
   omega.
@@ -555,7 +555,7 @@ Qed.
 Definition Zdivide_dec:
   forall (p q: Z), p > 0 -> { (p|q) } + { ~(p|q) }.
 Proof.
-  intros. destruct (zeq (Zmod q p) 0).
+  intros. destruct (zeq (Z.modulo q p) 0).
   left. exists (q / p).
   transitivity (p * (q / p) + (q mod p)). apply Z_div_mod_eq; auto.
   transitivity (p * (q / p)). omega. ring.
@@ -579,21 +579,21 @@ Qed.
 Definition nat_of_Z: Z -> nat := Z.to_nat.
 
 Lemma nat_of_Z_of_nat:
-  forall n, nat_of_Z (Z_of_nat n) = n.
+  forall n, nat_of_Z (Z.of_nat n) = n.
 Proof.
   exact Nat2Z.id.
 Qed.
 
 Lemma nat_of_Z_max:
-  forall z, Z_of_nat (nat_of_Z z) = Zmax z 0.
+  forall z, Z.of_nat (nat_of_Z z) = Z.max z 0.
 Proof.
-  intros. unfold Zmax. destruct z; simpl; auto.
+  intros. unfold Z.max. destruct z; simpl; auto.
   change (Z.of_nat (Z.to_nat (Zpos p)) = Zpos p).
   apply Z2Nat.id. compute; intuition congruence.
 Qed.
 
 Lemma nat_of_Z_eq:
-  forall z, z >= 0 -> Z_of_nat (nat_of_Z z) = z.
+  forall z, z >= 0 -> Z.of_nat (nat_of_Z z) = z.
 Proof.
   unfold nat_of_Z; intros. apply Z2Nat.id. omega.
 Qed.
@@ -601,7 +601,7 @@ Qed.
 Lemma nat_of_Z_neg:
   forall n, n <= 0 -> nat_of_Z n = O.
 Proof.
-  destruct n; unfold Zle; simpl; auto. congruence.
+  destruct n; unfold Z.le; simpl; auto. congruence.
 Qed.
 
 Lemma nat_of_Z_plus:
@@ -626,12 +626,12 @@ Proof.
   replace ((x + y - 1) / y * y)
      with ((x + y - 1) - (x + y - 1) mod y).
   generalize (Z_mod_lt (x + y - 1) y H). omega.
-  rewrite Zmult_comm. omega.
+  rewrite Z.mul_comm. omega.
 Qed.
 
 Lemma align_divides: forall x y, y > 0 -> (y | align x y).
 Proof.
-  intros. unfold align. apply Zdivide_factor_l.
+  intros. unfold align. apply Z.divide_factor_r.
 Qed.
 
 (** * Definitions and theorems on the data types [option], [sum] and [list] *)
@@ -697,7 +697,7 @@ Hint Resolve nth_error_nil: coqlib.
 Fixpoint list_length_z_aux (A: Type) (l: list A) (acc: Z) {struct l}: Z :=
   match l with
   | nil => acc
-  | hd :: tl => list_length_z_aux tl (Zsucc acc)
+  | hd :: tl => list_length_z_aux tl (Z.succ acc)
   end.
 
 Remark list_length_z_aux_shift:
@@ -706,7 +706,7 @@ Remark list_length_z_aux_shift:
 Proof.
   induction l; intros; simpl.
   omega.
-  replace (n - m) with (Zsucc n - Zsucc m) by omega. auto.
+  replace (n - m) with (Z.succ n - Z.succ m) by omega. auto.
 Qed.
 
 Definition list_length_z (A: Type) (l: list A) : Z :=
@@ -741,7 +741,7 @@ Qed.
 Fixpoint list_nth_z (A: Type) (l: list A) (n: Z) {struct l}: option A :=
   match l with
   | nil => None
-  | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Zpred n)
+  | hd :: tl => if zeq n 0 then Some hd else list_nth_z tl (Z.pred n)
   end.
 
 Lemma list_nth_z_in:
@@ -998,7 +998,7 @@ Lemma list_disjoint_sym:
   list_disjoint l1 l2 -> list_disjoint l2 l1.
 Proof.
   unfold list_disjoint; intros.
-  apply sym_not_equal. apply H; auto.
+  apply not_eq_sym. apply H; auto.
 Qed.
 
 Lemma list_disjoint_dec:
diff --git a/lib/Decidableplus.v b/lib/Decidableplus.v
index 6383794d..66dffb3a 100644
--- a/lib/Decidableplus.v
+++ b/lib/Decidableplus.v
@@ -86,10 +86,10 @@ Next Obligation.
 Qed.
 
 Program Instance Decidable_eq_nat : forall (x y : nat), Decidable (eq x y) := {
-  Decidable_witness := beq_nat x y
+  Decidable_witness := Nat.eqb x y
 }.
 Next Obligation.
-  apply beq_nat_true_iff.
+  apply Nat.eqb_eq.
 Qed.
 
 Program Instance Decidable_eq_positive : forall (x y : positive), Decidable (eq x y) := {
diff --git a/lib/Fappli_IEEE_extra.v b/lib/Fappli_IEEE_extra.v
index c134a3b6..85fadc16 100644
--- a/lib/Fappli_IEEE_extra.v
+++ b/lib/Fappli_IEEE_extra.v
@@ -104,15 +104,15 @@ Proof.
   destruct f1 as [| |? []|], f2 as [| |? []|];
   try destruct b; try destruct b0;
   try solve [left; auto]; try_not_eq.
-  destruct (positive_eq_dec x x0); try_not_eq;
+  destruct (Pos.eq_dec x x0); try_not_eq;
     subst; left; f_equal; f_equal; apply UIP_bool.
-  destruct (positive_eq_dec x x0); try_not_eq;
+  destruct (Pos.eq_dec x x0); try_not_eq;
     subst; left; f_equal; f_equal; apply UIP_bool.
-  destruct (positive_eq_dec m m0); try_not_eq;
-  destruct (Z_eq_dec e e1); try solve [right; intro H; inversion H; congruence];
+  destruct (Pos.eq_dec m m0); try_not_eq;
+  destruct (Z.eq_dec e e1); try solve [right; intro H; inversion H; congruence];
   subst; left; f_equal; apply UIP_bool.
-  destruct (positive_eq_dec m m0); try_not_eq;
-  destruct (Z_eq_dec e e1); try solve [right; intro H; inversion H; congruence];
+  destruct (Pos.eq_dec m m0); try_not_eq;
+  destruct (Z.eq_dec e e1); try solve [right; intro H; inversion H; congruence];
   subst; left; f_equal; apply UIP_bool.
 Defined.
 
@@ -155,7 +155,7 @@ Proof.
   intros; split.
 - red in prec_gt_0_.
   rewrite Z.abs_eq by (apply (Zpower_ge_0 radix2)).
-  apply Zle_trans with (2^(emax-1)).
+  apply Z.le_trans with (2^(emax-1)).
   apply (Zpower_le radix2); omega.
   assert (2^emax = 2^(emax-1)*2).
   { change 2 with (2^1) at 3. rewrite <- (Zpower_plus radix2) by omega.
@@ -233,9 +233,9 @@ Theorem BofZ_correct:
   then
     B2R prec emax (BofZ n) = round radix2 fexp (round_mode mode_NE) (Z2R n) /\
     is_finite _ _ (BofZ n) = true /\
-    Bsign prec emax (BofZ n) = Zlt_bool n 0
+    Bsign prec emax (BofZ n) = Z.ltb n 0
   else
-    B2FF prec emax (BofZ n) = binary_overflow prec emax mode_NE (Zlt_bool n 0).
+    B2FF prec emax (BofZ n) = binary_overflow prec emax mode_NE (Z.ltb n 0).
 Proof.
   intros.
   generalize (binary_normalize_correct prec emax prec_gt_0_ Hmax mode_NE n 0 false).
@@ -246,9 +246,9 @@ Proof.
   + auto.
   + auto.
   + rewrite C. change 0%R with (Z2R 0). rewrite Rcompare_Z2R.
-    unfold Zlt_bool. auto.
+    unfold Z.ltb. auto.
 - intros A; rewrite A. f_equal. change 0%R with (Z2R 0).
-  generalize (Zlt_bool_spec n 0); intros SPEC; inversion SPEC.
+  generalize (Z.ltb_spec n 0); intros SPEC; inversion SPEC.
   apply Rlt_bool_true; apply Z2R_lt; auto.
   apply Rlt_bool_false; apply Z2R_le; auto.
 - unfold F2R; simpl. ring.
@@ -259,7 +259,7 @@ Theorem BofZ_finite:
   Z.abs n <= 2^emax - 2^(emax-prec) ->
   B2R _ _ (BofZ n) = round radix2 fexp (round_mode mode_NE) (Z2R n)
   /\ is_finite _ _ (BofZ n) = true
-  /\ Bsign _ _ (BofZ n) = Zlt_bool n 0%Z.
+  /\ Bsign _ _ (BofZ n) = Z.ltb n 0%Z.
 Proof.
   intros.
   generalize (BofZ_correct n). rewrite Rlt_bool_true. auto.
@@ -282,7 +282,7 @@ Theorem BofZ_exact:
   -2^prec <= n <= 2^prec ->
   B2R _ _ (BofZ n) = Z2R n
   /\ is_finite _ _ (BofZ n) = true
-  /\ Bsign _ _ (BofZ n) = Zlt_bool n 0%Z.
+  /\ Bsign _ _ (BofZ n) = Z.ltb n 0%Z.
 Proof.
   intros. apply BofZ_representable. apply integer_representable_n; auto.
 Qed.
@@ -340,7 +340,7 @@ Proof.
   apply B2R_Bsign_inj; auto.
   rewrite P, U; auto.
   rewrite R, W, C, F.
-  change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Zlt_bool at 3.
+  change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Z.ltb at 3.
   generalize (Zcompare_spec (p + q) 0); intros SPEC; inversion SPEC; auto.
   assert (EITHER: 0 <= p \/ 0 <= q) by omega.
   destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2];
@@ -370,7 +370,7 @@ Proof.
   apply B2R_Bsign_inj; auto.
   rewrite P, U; auto.
   rewrite R, W, C, F.
-  change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Zlt_bool at 3.
+  change 0%R with (Z2R 0). rewrite Rcompare_Z2R. unfold Z.ltb at 3.
   generalize (Zcompare_spec (p - q) 0); intros SPEC; inversion SPEC; auto.
   assert (EITHER: 0 <= p \/ q < 0) by omega.
   destruct EITHER; [apply andb_false_intro1 | apply andb_false_intro2].
@@ -554,7 +554,7 @@ Lemma Zrnd_odd_int:
 Proof.
   intros.
   assert (0 < 2^p) by (apply (Zpower_gt_0 radix2); omega).
-  assert (n = (n / 2^p) * 2^p + n mod 2^p) by (rewrite Zmult_comm; apply Z.div_mod; omega).
+  assert (n = (n / 2^p) * 2^p + n mod 2^p) by (rewrite Z.mul_comm; apply Z.div_mod; omega).
   assert (0 <= n mod 2^p < 2^p) by (apply Z_mod_lt; omega).
   unfold int_round_odd. set (q := n / 2^p) in *; set (r := n mod 2^p) in *.
   f_equal.
@@ -606,8 +606,8 @@ Lemma int_round_odd_exact:
   (2^p | x) -> int_round_odd x p = x.
 Proof.
   intros. unfold int_round_odd. apply Znumtheory.Zdivide_mod in H0.
-  rewrite H0. simpl. rewrite Zmult_comm. symmetry. apply Z_div_exact_2.
-  apply Zlt_gt. apply (Zpower_gt_0 radix2). auto. auto.
+  rewrite H0. simpl. rewrite Z.mul_comm. symmetry. apply Z_div_exact_2.
+  apply Z.lt_gt. apply (Zpower_gt_0 radix2). auto. auto.
 Qed.
 
 Theorem BofZ_round_odd:
@@ -693,9 +693,9 @@ Qed.
 
 Definition ZofB (f: binary_float): option Z :=
   match f with
-    | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Zpower_pos radix2 e)%Z
+    | B754_finite _ _ s m (Zpos e) _ => Some (cond_Zopp s (Zpos m) * Z.pow_pos radix2 e)%Z
     | B754_finite _ _ s m 0 _ => Some (cond_Zopp s (Zpos m))
-    | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Zpower_pos radix2 e))%Z
+    | B754_finite _ _ s m (Zneg e) _ => Some (cond_Zopp s (Zpos m / Z.pow_pos radix2 e))%Z
     | B754_zero _ _ _ => Some 0%Z
     | _ => None
   end.
@@ -715,7 +715,7 @@ Proof.
       intros. destruct b; simpl; auto. apply Ztrunc_opp.
     }
     rewrite EQ. f_equal.
-    generalize (Zpower_pos_gt_0 2 p (refl_equal _)); intros.
+    generalize (Zpower_pos_gt_0 2 p (eq_refl _)); intros.
     rewrite Ztrunc_floor. symmetry. apply Zfloor_div. omega.
     apply Rmult_le_pos. apply (Z2R_le 0). compute; congruence.
     apply Rlt_le. apply Rinv_0_lt_compat. apply (Z2R_lt 0). auto.
@@ -844,14 +844,14 @@ Qed.
 Definition ZofB_range (f: binary_float) (zmin zmax: Z): option Z :=
   match ZofB f with
   | None => None
-  | Some z => if Zle_bool zmin z && Zle_bool z zmax then Some z else None
+  | Some z => if Z.leb zmin z && Z.leb z zmax then Some z else None
   end.
 
 Theorem ZofB_range_correct:
   forall f min max,
   let n := Ztrunc (B2R _ _ f) in
   ZofB_range f min max =
-  if is_finite _ _ f && Zle_bool min n && Zle_bool n max then Some n else None.
+  if is_finite _ _ f && Z.leb min n && Z.leb n max then Some n else None.
 Proof.
   intros. unfold ZofB_range. rewrite ZofB_correct. fold n.
   destruct (is_finite prec emax f); auto.
@@ -910,8 +910,8 @@ Proof.
 - rewrite NAN; auto.
 - rewrite NAN; auto.
 - rewrite NAN; auto.
-- generalize (H (refl_equal _) (refl_equal _)); clear H.
-  generalize (H0 (refl_equal _) (refl_equal _)); clear H0.
+- generalize (H (eq_refl _) (eq_refl _)); clear H.
+  generalize (H0 (eq_refl _) (eq_refl _)); clear H0.
   fold emin. fold fexp.
   set (x := B754_finite prec emax b0 m0 e1 e2). set (rx := B2R _ _ x).
   set (y := B754_finite prec emax b m e e0). set (ry := B2R _ _ y).
@@ -1007,7 +1007,7 @@ Proof.
   assert (REC: forall n, Z.pos (nat_rect _ xH (fun _ => xO) n) = 2 ^ (Z.of_nat n)).
   { induction n. reflexivity.
     simpl nat_rect. transitivity (2 * Z.pos (nat_rect _ xH (fun _ => xO) n)). reflexivity.
-    rewrite inj_S. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega.
+    rewrite Nat2Z.inj_succ. rewrite IHn. unfold Z.succ. rewrite Zpower_plus by omega.
     change (2 ^ 1) with 2. ring. }
   red in prec_gt_0_.
   unfold Bexact_inverse_mantissa. rewrite iter_nat_of_Z by omega. rewrite REC.
@@ -1042,7 +1042,7 @@ Qed.
 Program Definition Bexact_inverse (f: binary_float) : option binary_float :=
   match f with
   | B754_finite _ _ s m e B =>
-      if positive_eq_dec m Bexact_inverse_mantissa then
+      if Pos.eq_dec m Bexact_inverse_mantissa then
       let e' := -e - (prec - 1) * 2 in
       if Z_le_dec emin e' then
       if Z_le_dec e' emax then
@@ -1171,7 +1171,7 @@ Proof.
   destruct (Z.log2_spec base) as [D E]; auto.
   destruct (Z.log2_up_spec base) as [F G]. apply radix_gt_1.
   assert (K: 0 <= 2 ^ Z.log2 base) by (apply Z.pow_nonneg; omega).
-  rewrite ! (Zmult_comm n). rewrite ! Z.pow_mul_r by omega.
+  rewrite ! (Z.mul_comm n). rewrite ! Z.pow_mul_r by omega.
   split; apply Z.pow_le_mono_l; omega.
 Qed.
 
@@ -1182,7 +1182,7 @@ Lemma bpow_log_pos:
 Proof.
   intros. rewrite <- ! Z2R_Zpower. apply Z2R_le; apply Zpower_log; auto.
   omega.
-  rewrite Zmult_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg.
+  rewrite Z.mul_comm; apply Zmult_gt_0_le_0_compat. omega. apply Z.log2_nonneg.
 Qed.
 
 Lemma bpow_log_neg:
@@ -1291,7 +1291,7 @@ Proof.
   rewrite pos_pow_spec. rewrite <- Z2R_Zpower by (zify; omega). rewrite <- Z2R_mult.
   replace false with (Z.pos m * Z.pos b ^ Z.pos e <? 0).
   exact (BofZ_correct (Z.pos m * Z.pos b ^ Z.pos e)).
-  rewrite Z.ltb_ge. rewrite Zmult_comm. apply Zmult_gt_0_le_0_compat. zify; omega.  apply (Zpower_ge_0 base).
+  rewrite Z.ltb_ge. rewrite Z.mul_comm. apply Zmult_gt_0_le_0_compat. zify; omega.  apply (Zpower_ge_0 base).
 + (* overflow *)
   rewrite Rlt_bool_false. auto. eapply Rle_trans; [idtac|apply Rle_abs].
   apply (round_integer_overflow base). zify; omega. auto.
@@ -1425,7 +1425,7 @@ Proof.
   destruct Rlt_bool.
 - intros (P & Q & R) (D & E & F). apply B2R_Bsign_inj; auto.
   congruence. rewrite F, C, R. change 0%R with (Z2R 0). rewrite Rcompare_Z2R.
-  unfold Zlt_bool. auto.
+  unfold Z.ltb. auto.
 - intros P Q. apply B2FF_inj. rewrite P, Q. rewrite C. f_equal. change 0%R with (Z2R 0).
   generalize (Zlt_bool_spec n 0); intros LT; inversion LT.
   rewrite Rlt_bool_true; auto. apply Z2R_lt; auto.
diff --git a/lib/Floats.v b/lib/Floats.v
index aa52b197..0c8ff5a4 100644
--- a/lib/Floats.v
+++ b/lib/Floats.v
@@ -92,10 +92,10 @@ Proof.
   destruct x as [[]|]; simpl; intros; discriminate.
 Qed.
 
-Local Notation __ := (refl_equal Datatypes.Lt).
+Local Notation __ := (eq_refl Datatypes.Lt).
 
-Local Hint Extern 1 (Prec_gt_0 _) => exact (refl_equal Datatypes.Lt).
-Local Hint Extern 1 (_ < _) => exact (refl_equal Datatypes.Lt).
+Local Hint Extern 1 (Prec_gt_0 _) => exact (eq_refl Datatypes.Lt).
+Local Hint Extern 1 (_ < _) => exact (eq_refl Datatypes.Lt).
 
 (** * Double-precision FP numbers *)
 
@@ -266,13 +266,13 @@ Ltac compute_this val :=
   let x := fresh in set val as x in *; vm_compute in x; subst x.
 
 Ltac smart_omega :=
-  simpl radix_val in *; simpl Zpower in *;
+  simpl radix_val in *; simpl Z.pow in *;
   compute_this Int.modulus; compute_this Int.half_modulus;
   compute_this Int.max_unsigned;
   compute_this Int.min_signed; compute_this Int.max_signed;
   compute_this Int64.modulus; compute_this Int64.half_modulus;
   compute_this Int64.max_unsigned;
-  compute_this (Zpower_pos 2 1024); compute_this (Zpower_pos 2 53); compute_this (Zpower_pos 2 52); compute_this (Zpower_pos 2 32);
+  compute_this (Z.pow_pos 2 1024); compute_this (Z.pow_pos 2 53); compute_this (Z.pow_pos 2 52); compute_this (Z.pow_pos 2 32);
   zify; omega.
 
 (** Commutativity properties of addition and multiplication. *)
@@ -510,10 +510,10 @@ Proof.
   intros; unfold from_words, of_bits, b64_of_bits, binary_float_of_bits.
   rewrite B2R_FF2B, is_finite_FF2B, Bsign_FF2B.
   unfold binary_float_of_bits_aux; rewrite split_bits_or; simpl; pose proof (Int.unsigned_range x).
-  destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?.
+  destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?.
   exfalso; now smart_omega.
   simpl; rewrite <- Heqz;  unfold F2R; simpl. split; auto.
-  rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Zplus_comm. auto.
+  rewrite <- (Z2R_plus 4503599627370496), Rmult_1_r. f_equal. rewrite Z.add_comm. auto.
   exfalso; now smart_omega.
 Qed.
 
@@ -593,11 +593,11 @@ Proof.
   intros; unfold from_words, of_bits, b64_of_bits, binary_float_of_bits.
   rewrite B2R_FF2B, is_finite_FF2B, Bsign_FF2B.
   unfold binary_float_of_bits_aux; rewrite split_bits_or'; simpl; pose proof (Int.unsigned_range x).
-  destruct (Int.unsigned x + Zpower_pos 2 52) eqn:?.
+  destruct (Int.unsigned x + Z.pow_pos 2 52) eqn:?.
   exfalso; now smart_omega.
   simpl; rewrite <- Heqz;  unfold F2R; simpl. split; auto.
   rewrite <- (Z2R_plus 19342813113834066795298816), <- (Z2R_mult _ 4294967296).
-  f_equal; compute_this (Zpower_pos 2 52); compute_this (two_power_pos 32); ring.
+  f_equal; compute_this (Z.pow_pos 2 52); compute_this (two_power_pos 32); ring.
   assert (Zneg p < 0) by reflexivity.
   exfalso; now smart_omega.
 Qed.
@@ -807,10 +807,10 @@ Proof.
   rewrite BofZ_mult_2p.
 - change (2^1) with 2. rewrite EQ. apply BofZ_round_odd with (p := 1).
 + omega.
-+ apply Zle_trans with Int64.modulus; trivial. smart_omega.
++ apply Z.le_trans with Int64.modulus; trivial. smart_omega.
 + omega.
-+ apply Zle_trans with (2^63). compute; intuition congruence. xomega.
-- apply Zle_trans with Int64.modulus; trivial.
++ apply Z.le_trans with (2^63). compute; intuition congruence. xomega.
+- apply Z.le_trans with Int64.modulus; trivial.
   pose proof (Int64.signed_range n).
   compute_this Int64.min_signed; compute_this Int64.max_signed;
   compute_this Int64.modulus; xomega.
@@ -1191,7 +1191,7 @@ Proof.
   assert (E: forall i, p < i -> Z.testbit m i = false).
   { intros. apply Z.testbit_false. omega.
     replace (m / 2^i) with 0. auto. symmetry. apply Zdiv_small.
-    unfold m. split. omega. apply Zlt_le_trans with (2 * 2^p). omega.
+    unfold m. split. omega. apply Z.lt_le_trans with (2 * 2^p). omega.
     change 2 with (2^1) at 1. rewrite <- (Zpower_plus radix2) by omega.
     apply Zpower_le. omega. }
   assert (F: forall i, 0 <= i -> Z.testbit (-2^p) i = if zlt i p then false else true).
@@ -1222,7 +1222,7 @@ Proof.
   rewrite Bconv_BofZ.
   apply BofZ_round_odd with (p := 11).
   omega.
-  apply Zle_trans with (2^64). omega. compute; intuition congruence.
+  apply Z.le_trans with (2^64). omega. compute; intuition congruence.
   omega.
   exact (proj1 H).
   unfold int_round_odd. apply integer_representable_n2p_wide. auto. omega.
@@ -1260,7 +1260,7 @@ Proof.
   assert (0 <= n').
   { rewrite <- H1. change 0 with (int_round_odd 0 11). apply (int_round_odd_le 0 0); omega. }
   assert (n' < Int64.modulus).
-  { apply Zle_lt_trans with (int_round_odd (Int64.modulus - 1) 11).
+  { apply Z.le_lt_trans with (int_round_odd (Int64.modulus - 1) 11).
     rewrite <- H1. apply (int_round_odd_le 0 0); omega.
     compute; auto. }
   rewrite <- (Int64.unsigned_repr n') by (unfold Int64.max_unsigned; omega).
@@ -1306,7 +1306,7 @@ Proof.
   assert (Int64.min_signed <= n').
   { rewrite <- H1. change Int64.min_signed with (int_round_odd Int64.min_signed 11). apply (int_round_odd_le 0 0); omega. }
   assert (n' <= Int64.max_signed).
-  { apply Zle_trans with (int_round_odd Int64.max_signed 11).
+  { apply Z.le_trans with (int_round_odd Int64.max_signed 11).
     rewrite <- H1. apply (int_round_odd_le 0 0); omega.
     compute; intuition congruence. }
   rewrite <- (Int64.signed_repr n') by omega.
@@ -1321,7 +1321,7 @@ Proof.
   change (Int64.unsigned (Int64.repr 2047)) with 2047.
   change 2047 with (Z.ones 11). rewrite ! Z.land_ones by omega.
   rewrite Int64.unsigned_repr. apply Int64.eqmod_mod_eq.
-  apply Zlt_gt. apply (Zpower_gt_0 radix2); omega.
+  apply Z.lt_gt. apply (Zpower_gt_0 radix2); omega.
   apply Int64.eqmod_divides with (2^64). apply Int64.eqm_signed_unsigned.
   exists (2^(64-11)); auto.
   exploit (Z_mod_lt (Int64.unsigned n) (2^11)). compute; auto.
diff --git a/lib/Integers.v b/lib/Integers.v
index 5fe8202d..b849872f 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -63,7 +63,7 @@ Local Unset Case Analysis Schemes.
 Module Make(WS: WORDSIZE).
 
 Definition wordsize: nat := WS.wordsize.
-Definition zwordsize: Z := Z_of_nat wordsize.
+Definition zwordsize: Z := Z.of_nat wordsize.
 Definition modulus : Z := two_power_nat wordsize.
 Definition half_modulus : Z := modulus / 2.
 Definition max_unsigned : Z := modulus - 1.
@@ -211,7 +211,7 @@ Proof.
   intros. subst y.
   assert (forall (n m: Z) (P1 P2: n < m), P1 = P2).
   {
-    unfold Zlt; intros.
+    unfold Z.lt; intros.
     apply eq_proofs_unicity.
     intros c1 c2. destruct c1; destruct c2; (left; reflexivity) || (right; congruence).
   }
@@ -423,8 +423,8 @@ Remark half_modulus_power:
 Proof.
   unfold half_modulus. rewrite modulus_power.
   set (ws1 := zwordsize - 1).
-  replace (zwordsize) with (Zsucc ws1).
-  rewrite two_p_S. rewrite Zmult_comm. apply Z_div_mult. omega.
+  replace (zwordsize) with (Z.succ ws1).
+  rewrite two_p_S. rewrite Z.mul_comm. apply Z_div_mult. omega.
   unfold ws1. generalize wordsize_pos; omega.
   unfold ws1. omega.
 Qed.
@@ -484,13 +484,13 @@ Proof.
 Qed.
 
 Lemma unsigned_repr_eq:
-  forall x, unsigned (repr x) = Zmod x modulus.
+  forall x, unsigned (repr x) = Z.modulo x modulus.
 Proof.
   intros. simpl. apply Z_mod_modulus_eq.
 Qed.
 
 Lemma signed_repr_eq:
-  forall x, signed (repr x) = if zlt (Zmod x modulus) half_modulus then Zmod x modulus else Zmod x modulus - modulus.
+  forall x, signed (repr x) = if zlt (Z.modulo x modulus) half_modulus then Z.modulo x modulus else Z.modulo x modulus - modulus.
 Proof.
   intros. unfold signed. rewrite unsigned_repr_eq. auto.
 Qed.
@@ -540,14 +540,14 @@ Lemma eqmod_mod_eq:
   forall x y, eqmod x y -> x mod modul = y mod modul.
 Proof.
   intros x y [k EQ]. subst x.
-  rewrite Zplus_comm. apply Z_mod_plus. auto.
+  rewrite Z.add_comm. apply Z_mod_plus. auto.
 Qed.
 
 Lemma eqmod_mod:
   forall x, eqmod x (x mod modul).
 Proof.
   intros; red. exists (x / modul).
-  rewrite Zmult_comm. apply Z_div_mod_eq. auto.
+  rewrite Z.mul_comm. apply Z_div_mod_eq. auto.
 Qed.
 
 Lemma eqmod_add:
@@ -582,10 +582,10 @@ Qed.
 End EQ_MODULO.
 
 Lemma eqmod_divides:
-  forall n m x y, eqmod n x y -> Zdivide m n -> eqmod m x y.
+  forall n m x y, eqmod n x y -> Z.divide m n -> eqmod m x y.
 Proof.
   intros. destruct H as [k1 EQ1]. destruct H0 as [k2 EQ2].
-  exists (k1*k2). rewrite <- Zmult_assoc. rewrite <- EQ2. auto.
+  exists (k1*k2). rewrite <- Z.mul_assoc. rewrite <- EQ2. auto.
 Qed.
 
 (** We then specialize these definitions to equality modulo
@@ -777,8 +777,8 @@ Qed.
 Theorem unsigned_one: unsigned one = 1.
 Proof.
   unfold one; rewrite unsigned_repr_eq. apply Zmod_small. split. omega.
-  unfold modulus. replace wordsize with (S(pred wordsize)).
-  rewrite two_power_nat_S. generalize (two_power_nat_pos (pred wordsize)).
+  unfold modulus. replace wordsize with (S(Init.Nat.pred wordsize)).
+  rewrite two_power_nat_S. generalize (two_power_nat_pos (Init.Nat.pred wordsize)).
   omega.
   generalize wordsize_pos. unfold zwordsize. omega.
 Qed.
@@ -879,7 +879,7 @@ Proof. intros; unfold add. decEq. omega. Qed.
 Theorem add_zero: forall x, add x zero = x.
 Proof.
   intros. unfold add. rewrite unsigned_zero.
-  rewrite Zplus_0_r. apply repr_unsigned.
+  rewrite Z.add_0_r. apply repr_unsigned.
 Qed.
 
 Theorem add_zero_l: forall x, add zero x = x.
@@ -896,7 +896,7 @@ Proof.
   apply eqm_samerepr.
   apply eqm_trans with ((x' + y') + z').
   auto with ints.
-  rewrite <- Zplus_assoc. auto with ints.
+  rewrite <- Z.add_assoc. auto with ints.
 Qed.
 
 Theorem add_permut: forall x y z, add x (add y z) = add y (add x z).
@@ -916,7 +916,7 @@ Theorem unsigned_add_carry:
   unsigned (add x y) = unsigned x + unsigned y - unsigned (add_carry x y zero) * modulus.
 Proof.
   intros.
-  unfold add, add_carry. rewrite unsigned_zero. rewrite Zplus_0_r.
+  unfold add, add_carry. rewrite unsigned_zero. rewrite Z.add_0_r.
   rewrite unsigned_repr_eq.
   generalize (unsigned_range x) (unsigned_range y). intros.
   destruct (zlt (unsigned x + unsigned y) modulus).
@@ -930,7 +930,7 @@ Corollary unsigned_add_either:
   \/ unsigned (add x y) = unsigned x + unsigned y - modulus.
 Proof.
   intros. rewrite unsigned_add_carry. unfold add_carry.
-  rewrite unsigned_zero. rewrite Zplus_0_r.
+  rewrite unsigned_zero. rewrite Z.add_0_r.
   destruct (zlt (unsigned x + unsigned y) modulus).
   rewrite unsigned_zero. left; omega.
   rewrite unsigned_one. right; omega.
@@ -1025,7 +1025,7 @@ Theorem unsigned_sub_borrow:
   unsigned (sub x y) = unsigned x - unsigned y + unsigned (sub_borrow x y zero) * modulus.
 Proof.
   intros.
-  unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Zminus_0_r.
+  unfold sub, sub_borrow. rewrite unsigned_zero. rewrite Z.sub_0_r.
   rewrite unsigned_repr_eq.
   generalize (unsigned_range x) (unsigned_range y). intros.
   destruct (zlt (unsigned x - unsigned y) 0).
@@ -1070,7 +1070,7 @@ Proof.
   set (z' := unsigned z).
   apply eqm_samerepr. apply eqm_trans with ((x' * y') * z').
   auto with ints.
-  rewrite <- Zmult_assoc. auto with ints.
+  rewrite <- Z.mul_assoc. auto with ints.
 Qed.
 
 Theorem mul_add_distr_l:
@@ -1130,7 +1130,7 @@ Proof.
   apply eqm_samerepr.
   set (x' := unsigned x). set (y' := unsigned y).
   apply eqm_trans with ((x' / y') * y' + x' mod y').
-  apply eqm_refl2. rewrite Zmult_comm. apply Z_div_mod_eq.
+  apply eqm_refl2. rewrite Z.mul_comm. apply Z_div_mod_eq.
   generalize (unsigned_range y); intro.
   assert (unsigned y <> 0). red; intro.
   elim H. rewrite <- (repr_unsigned y). unfold zero. congruence.
@@ -1156,7 +1156,7 @@ Proof.
   apply eqm_samerepr.
   set (x' := signed x). set (y' := signed y).
   apply eqm_trans with ((Z.quot x' y') * y' + Z.rem x' y').
-  apply eqm_refl2. rewrite Zmult_comm. apply Z.quot_rem'.
+  apply eqm_refl2. rewrite Z.mul_comm. apply Z.quot_rem'.
   apply eqm_add; auto with ints.
   apply eqm_unsigned_repr_r. apply eqm_mult; auto with ints.
   unfold y'. apply eqm_signed_unsigned.
@@ -1280,7 +1280,7 @@ Proof.
     assert (Z.abs (Z.quot N D) < half_modulus).
     { rewrite <- Z.quot_abs by omega. apply Zquot_lt_upper_bound.
       xomega. xomega.
-      apply Zle_lt_trans with (half_modulus * 1).
+      apply Z.le_lt_trans with (half_modulus * 1).
       rewrite Z.mul_1_r. unfold min_signed, max_signed in H3; xomega.
       apply Zmult_lt_compat_l. generalize half_modulus_pos; omega. xomega. }
     rewrite Z.abs_lt in H4.
@@ -1344,13 +1344,13 @@ Proof.
   intros. rewrite Zshiftin_spec. destruct (zeq n 0).
   - subst n. destruct b.
     + apply Z.testbit_odd_0.
-    + rewrite Zplus_0_r. apply Z.testbit_even_0.
+    + rewrite Z.add_0_r. apply Z.testbit_even_0.
   - assert (0 <= Z.pred n) by omega.
     set (n' := Z.pred n) in *.
     replace n with (Z.succ n') by (unfold n'; omega).
     destruct b.
     + apply Z.testbit_odd_succ; auto.
-    + rewrite Zplus_0_r. apply Z.testbit_even_succ; auto.
+    + rewrite Z.add_0_r. apply Z.testbit_even_succ; auto.
 Qed.
 
 Remark Ztestbit_shiftin_base:
@@ -1395,13 +1395,13 @@ Proof.
   - change (two_power_nat 0) with 1. exists (x-y); ring.
   - rewrite two_power_nat_S.
     assert (eqmod (two_power_nat n) (Z.div2 x) (Z.div2 y)).
-      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite inj_S; omega.
+      apply IHn. intros. rewrite <- !Ztestbit_succ. apply H. rewrite Nat2Z.inj_succ; omega.
       omega. omega.
   destruct H0 as [k EQ].
   exists k. rewrite (Zdecomp x). rewrite (Zdecomp y).
   replace (Z.odd y) with (Z.odd x).
   rewrite EQ. rewrite !Zshiftin_spec. ring.
-  exploit (H 0). rewrite inj_S; omega.
+  exploit (H 0). rewrite Nat2Z.inj_succ; omega.
   rewrite !Ztestbit_base. auto.
 Qed.
 
@@ -1418,7 +1418,7 @@ Lemma same_bits_eqmod:
 Proof.
   induction n; intros.
   - simpl in H0. omegaContradiction.
-  - rewrite inj_S in H0. rewrite two_power_nat_S in H.
+  - rewrite Nat2Z.inj_succ in H0. rewrite two_power_nat_S in H.
     rewrite !(Ztestbit_eq i); intuition.
     destruct H as [k EQ].
     assert (EQ': Zshiftin (Z.odd x) (Z.div2 x) =
@@ -1494,7 +1494,7 @@ Proof.
   - change (two_power_nat 0) with 1 in H.
     replace x with 0 by omega.
     apply Z.testbit_0_l.
-  - rewrite inj_S in H0. rewrite Ztestbit_eq. rewrite zeq_false.
+  - rewrite Nat2Z.inj_succ in H0. rewrite Ztestbit_eq. rewrite zeq_false.
     apply IHn. rewrite two_power_nat_S in H. rewrite (Zdecomp x) in H.
     rewrite Zshiftin_spec in H. destruct (Z.odd x); omega.
     omega. omega. omega.
@@ -1518,13 +1518,13 @@ Qed.
 Lemma Zsign_bit:
   forall n x,
   0 <= x < two_power_nat (S n) ->
-  Z.testbit x (Z_of_nat n) = if zlt x (two_power_nat n) then false else true.
+  Z.testbit x (Z.of_nat n) = if zlt x (two_power_nat n) then false else true.
 Proof.
   induction n; intros.
   - change (two_power_nat 1) with 2 in H.
     assert (x = 0 \/ x = 1) by omega.
     destruct H0; subst x; reflexivity.
-  - rewrite inj_S. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ.
+  - rewrite Nat2Z.inj_succ. rewrite Ztestbit_eq. rewrite zeq_false. rewrite Z.pred_succ.
     rewrite IHn. rewrite two_power_nat_S.
     destruct (zlt (Z.div2 x) (two_power_nat n)); rewrite (Zdecomp x); rewrite Zshiftin_spec.
     rewrite zlt_true. auto. destruct (Z.odd x); omega.
@@ -1573,7 +1573,7 @@ Proof.
     rewrite Ztestbit_0. destruct (Z.testbit x i) as [] eqn:E; auto.
     exploit H; eauto. rewrite Ztestbit_0. auto.
   - assert (Z.div2 x0 <= x).
-    { apply H0. intros. exploit (H1 (Zsucc i)).
+    { apply H0. intros. exploit (H1 (Z.succ i)).
         omega. rewrite Ztestbit_succ; auto. rewrite Ztestbit_shiftin_succ; auto.
     }
     rewrite (Zdecomp x0). rewrite !Zshiftin_spec.
@@ -1635,12 +1635,12 @@ Lemma sign_bit_of_unsigned:
   forall x, testbit x (zwordsize - 1) = if zlt (unsigned x) half_modulus then false else true.
 Proof.
   intros. unfold testbit.
-  set (ws1 := pred wordsize).
-  assert (zwordsize - 1 = Z_of_nat ws1).
+  set (ws1 := Init.Nat.pred wordsize).
+  assert (zwordsize - 1 = Z.of_nat ws1).
     unfold zwordsize, ws1, wordsize.
     destruct WS.wordsize as [] eqn:E.
     elim WS.wordsize_not_zero; auto.
-    rewrite inj_S. simpl. omega.
+    rewrite Nat2Z.inj_succ. simpl. omega.
   assert (half_modulus = two_power_nat ws1).
     rewrite two_power_nat_two_p. rewrite <- H. apply half_modulus_power.
   rewrite H; rewrite H0.
@@ -2346,7 +2346,7 @@ Proof.
   rewrite bits_shru; auto.
   rewrite unsigned_repr.
   destruct (zeq i 0).
-  subst i. rewrite Zplus_0_l. rewrite zlt_true.
+  subst i. rewrite Z.add_0_l. rewrite zlt_true.
   rewrite sign_bit_of_unsigned.
   unfold lt. rewrite signed_zero. unfold signed.
   destruct (zlt (unsigned x) half_modulus).
@@ -2478,7 +2478,7 @@ Theorem rol_zero:
   forall x,
   rol x zero = x.
 Proof.
-  bit_solve. f_equal. rewrite unsigned_zero. rewrite Zminus_0_r.
+  bit_solve. f_equal. rewrite unsigned_zero. rewrite Z.sub_0_r.
   apply Zmod_small; auto.
 Qed.
 
@@ -2515,7 +2515,7 @@ Qed.
 
 Theorem rol_rol:
   forall x n m,
-  Zdivide zwordsize modulus ->
+  Z.divide zwordsize modulus ->
   rol (rol x n) m = rol x (modu (add n m) iwordsize).
 Proof.
   bit_solve. f_equal. apply eqmod_mod_eq. apply wordsize_pos.
@@ -2527,7 +2527,7 @@ Proof.
   replace (i - M - N) with (i - (M + N)) by omega.
   apply eqmod_sub.
   apply eqmod_refl.
-  apply eqmod_trans with (Zmod (unsigned n + unsigned m) zwordsize).
+  apply eqmod_trans with (Z.modulo (unsigned n + unsigned m) zwordsize).
   replace (M + N) with (N + M) by omega. apply eqmod_mod. apply wordsize_pos.
   unfold modu, add. fold M; fold N. rewrite unsigned_repr_wordsize.
   assert (forall a, eqmod zwordsize a (unsigned (repr a))).
@@ -2546,7 +2546,7 @@ Qed.
 
 Theorem rolm_rolm:
   forall x n1 m1 n2 m2,
-  Zdivide zwordsize modulus ->
+  Z.divide zwordsize modulus ->
   rolm (rolm x n1 m1) n2 m2 =
     rolm x (modu (add n1 n2) iwordsize)
            (and (rol m1 n2) m2).
@@ -2651,11 +2651,11 @@ Lemma Z_one_bits_range:
   forall x i, In i (Z_one_bits wordsize x 0) -> 0 <= i < zwordsize.
 Proof.
   assert (forall n x i j,
-    In j (Z_one_bits n x i) -> i <= j < i + Z_of_nat n).
+    In j (Z_one_bits n x i) -> i <= j < i + Z.of_nat n).
   {
   induction n; simpl In.
   tauto.
-  intros x i j. rewrite inj_S.
+  intros x i j. rewrite Nat2Z.inj_succ.
   assert (In j (Z_one_bits n (Z.div2 x) (i + 1)) -> i <= j < i + Z.succ (Z.of_nat n)).
     intros. exploit IHn; eauto. omega.
   destruct (Z.odd x); simpl.
@@ -2729,16 +2729,16 @@ Qed.
 
 Remark Z_one_bits_two_p:
   forall n x i,
-  0 <= x < Z_of_nat n ->
+  0 <= x < Z.of_nat n ->
   Z_one_bits n (two_p x) i = (i + x) :: nil.
 Proof.
   induction n; intros; simpl. simpl in H. omegaContradiction.
-  rewrite inj_S in H.
+  rewrite Nat2Z.inj_succ in H.
   assert (x = 0 \/ 0 < x) by omega. destruct H0.
   subst x; simpl. decEq. omega. apply Z_one_bits_zero.
   assert (Z.odd (two_p x) = false /\ Z.div2 (two_p x) = two_p (x-1)).
     apply Zshiftin_inj. rewrite <- Zdecomp. rewrite !Zshiftin_spec.
-    rewrite <- two_p_S. rewrite Zplus_0_r. f_equal; omega. omega.
+    rewrite <- two_p_S. rewrite Z.add_0_r. f_equal; omega. omega.
   destruct H1 as [A B]; rewrite A; rewrite B.
   rewrite IHn. f_equal; omega. omega.
 Qed.
@@ -2838,7 +2838,7 @@ Proof.
     + intros. rewrite Pos.iter_succ. rewrite H0.
       rewrite Pplus_one_succ_l. rewrite two_power_pos_is_exp.
       change (two_power_pos 1) with 2.
-      rewrite Zdiv2_div. rewrite Zmult_comm. apply Zdiv_Zdiv.
+      rewrite Zdiv2_div. rewrite Z.mul_comm. apply Zdiv_Zdiv.
       rewrite two_power_pos_nat. apply two_power_nat_pos. omega.
   - compute in H. congruence.
 Qed.
@@ -2904,7 +2904,7 @@ Proof.
       * omega.
     + rewrite (Zdecomp x0) at 3. set (x1 := Z.div2 x0). symmetry.
       apply Zmod_unique with (x1 / two_p x).
-      rewrite !Zshiftin_spec. rewrite Zplus_assoc. f_equal.
+      rewrite !Zshiftin_spec. rewrite Z.add_assoc. f_equal.
       transitivity (2 * (two_p x * (x1 / two_p x) + x1 mod two_p x)).
       f_equal. apply Z_div_mod_eq. apply two_p_gt_ZERO; auto.
       ring.
@@ -3038,7 +3038,7 @@ Qed.
 
 Lemma Zdiv_shift:
   forall x y, y > 0 ->
-  (x + (y - 1)) / y = x / y + if zeq (Zmod x y) 0 then 0 else 1.
+  (x + (y - 1)) / y = x / y + if zeq (Z.modulo x y) 0 then 0 else 1.
 Proof.
   intros. generalize (Z_div_mod_eq x y H). generalize (Z_mod_lt x y H).
   set (q := x / y). set (r := x mod y). intros.
@@ -3258,7 +3258,7 @@ Qed.
 
 Theorem zero_ext_mod:
   forall n x, 0 <= n < zwordsize ->
-  unsigned (zero_ext n x) = Zmod (unsigned x) (two_p n).
+  unsigned (zero_ext n x) = Z.modulo (unsigned x) (two_p n).
 Proof.
   intros. apply equal_same_bits. intros.
   rewrite Ztestbit_mod_two_p; auto.
@@ -3651,7 +3651,7 @@ Theorem lt_sub_overflow:
   xor (sub_overflow x y zero) (negative (sub x y)) = if lt x y then one else zero.
 Proof.
   intros. unfold negative, sub_overflow, lt. rewrite sub_signed.
-  rewrite signed_zero. rewrite Zminus_0_r.
+  rewrite signed_zero. rewrite Z.sub_0_r.
   generalize (signed_range x) (signed_range y).
   set (X := signed x); set (Y := signed y). intros RX RY.
   unfold min_signed, max_signed in *.
@@ -3777,7 +3777,7 @@ Proof.
 Qed.
 
 Lemma Zsize_shiftin:
-  forall b x, 0 < x -> Zsize (Zshiftin b x) = Zsucc (Zsize x).
+  forall b x, 0 < x -> Zsize (Zshiftin b x) = Z.succ (Zsize x).
 Proof.
   intros. destruct x; compute in H; try discriminate.
   destruct b.
@@ -3788,7 +3788,7 @@ Proof.
 Qed.
 
 Lemma Ztestbit_size_1:
-  forall x, 0 < x -> Z.testbit x (Zpred (Zsize x)) = true.
+  forall x, 0 < x -> Z.testbit x (Z.pred (Zsize x)) = true.
 Proof.
   intros x0 POS0; pattern x0; apply Zshiftin_pos_ind; auto.
   intros. rewrite Zsize_shiftin; auto.
@@ -3832,14 +3832,14 @@ Proof.
   destruct (zeq x 0).
   subst x; simpl; omega.
   destruct (zlt n (Zsize x)); auto.
-  exploit (Ztestbit_above N x (Zpred (Zsize x))). auto. omega.
+  exploit (Ztestbit_above N x (Z.pred (Zsize x))). auto. omega.
   rewrite Ztestbit_size_1. congruence. omega.
 Qed.
 
 Lemma Zsize_monotone:
   forall x y, 0 <= x <= y -> Zsize x <= Zsize y.
 Proof.
-  intros. apply Zge_le. apply Zsize_interval_2. apply Zsize_pos.
+  intros. apply Z.ge_le. apply Zsize_interval_2. apply Zsize_pos.
   exploit (Zsize_interval_1 y). omega.
   omega.
 Qed.
@@ -3850,7 +3850,7 @@ Proof.
 Qed.
 
 Theorem bits_size_1:
-  forall x, x = zero \/ testbit x (Zpred (size x)) = true.
+  forall x, x = zero \/ testbit x (Z.pred (size x)) = true.
 Proof.
   intros. destruct (zeq (unsigned x) 0).
   left. rewrite <- (repr_unsigned x). rewrite e; auto.
@@ -3890,7 +3890,7 @@ Qed.
 Theorem bits_size_4:
   forall x n,
   0 <= n ->
-  testbit x (Zpred n) = true ->
+  testbit x (Z.pred n) = true ->
   (forall i, n <= i < zwordsize -> testbit x i = false) ->
   size x = n.
 Proof.
@@ -4005,7 +4005,7 @@ Strategy 0 [Wordsize_32.wordsize].
 Notation int := Int.int.
 
 Remark int_wordsize_divides_modulus:
-  Zdivide (Z_of_nat Int.wordsize) Int.modulus.
+  Z.divide (Z.of_nat Int.wordsize) Int.modulus.
 Proof.
   exists (two_p (32-5)); reflexivity.
 Qed.
@@ -4799,7 +4799,7 @@ Proof.
   set (p := Int.unsigned x * Int.unsigned y).
   set (ph := p / Int.modulus). set (pl := p mod Int.modulus).
   transitivity (repr (ph * Int.modulus + pl)).
-- f_equal. rewrite Zmult_comm. apply Z_div_mod_eq. apply Int.modulus_pos.
+- f_equal. rewrite Z.mul_comm. apply Z_div_mod_eq. apply Int.modulus_pos.
 - apply eqm_samerepr. apply eqm_add. apply eqm_mul_2p32. auto with ints.
   rewrite Int.unsigned_repr_eq. apply eqm_refl.
 Qed.
@@ -4832,7 +4832,7 @@ Proof.
   apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl.
   unfold mul'. apply eqm_unsigned_repr_l. apply eqm_refl.
   transitivity (repr (0 + (XL * YL + (XL * YH + XH * YL) * two_p 32))).
-  rewrite Zplus_0_l; auto.
+  rewrite Z.add_0_l; auto.
   transitivity (repr (XH * YH * (two_p 32 * two_p 32) + (XL * YL + (XL * YH + XH * YL) * two_p 32))).
   apply eqm_samerepr. apply eqm_add. 2: apply eqm_refl.
   change (two_p 32 * two_p 32) with modulus. exists (- XH * YH). ring.
diff --git a/lib/Iteration.v b/lib/Iteration.v
index 4398f96d..6a9d3253 100644
--- a/lib/Iteration.v
+++ b/lib/Iteration.v
@@ -146,7 +146,7 @@ Definition iter_step (x: positive)
   | right NOTEQ =>
       match step s with
       | inl res => Some res
-      | inr s'  => next (Ppred x) (Ppred_Plt x NOTEQ) s'
+      | inr s'  => next (Pos.pred x) (Ppred_Plt x NOTEQ) s'
       end
   end.
 
@@ -176,7 +176,7 @@ Proof.
   specialize (step_prop a H0).
   destruct (step a) as [b'|a'] eqn:?.
   inv H1. auto.
-  apply H with (Ppred x) a'. apply Ppred_Plt; auto. auto. auto.
+  apply H with (Pos.pred x) a'. apply Ppred_Plt; auto. auto. auto.
 Qed.
 
 Lemma iterate_prop:
diff --git a/lib/Lattice.v b/lib/Lattice.v
index 6eebca99..b7ae837b 100644
--- a/lib/Lattice.v
+++ b/lib/Lattice.v
@@ -662,9 +662,9 @@ Inductive t' : Type :=
 Definition t : Type := t'.
 
 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 :=
   match x, y with
@@ -746,9 +746,9 @@ Module LBoolean <: SEMILATTICE_WITH_TOP.
 Definition t := bool.
 
 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 : t -> t -> bool := eqb.
 
diff --git a/lib/Ordered.v b/lib/Ordered.v
index a2c36673..c333cc50 100644
--- a/lib/Ordered.v
+++ b/lib/Ordered.v
@@ -31,11 +31,11 @@ Definition eq (x y: t) := x = y.
 Definition lt := Plt.
 
 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 Plt_trans.
 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
@@ -58,16 +58,16 @@ Module OrderedZ <: OrderedType.
 
 Definition t := Z.
 Definition eq (x y: t) := x = y.
-Definition lt := Zlt.
+Definition lt := Z.lt.
 
 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 Zlt_trans.
+Proof Z.lt_trans.
 Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y.
 Proof. unfold lt, eq, t; intros. omega. Qed.
 Lemma compare : forall x y : t, Compare lt eq x y.
@@ -91,11 +91,11 @@ Definition eq (x y: t) := x = y.
 Definition lt (x y: t) := Int.unsigned x < Int.unsigned 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. omega.
@@ -129,11 +129,11 @@ Definition eq (x y: t) := x = y.
 Definition lt (x y: t) := Plt (A.index x) (A.index 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.
diff --git a/lib/Parmov.v b/lib/Parmov.v
index 92bba559..2d09171d 100644
--- a/lib/Parmov.v
+++ b/lib/Parmov.v
@@ -1564,7 +1564,7 @@ Proof.
   subst. rewrite update_s. rewrite weak_update_s. apply H1.
   destruct H. apply no_adherence_src; auto. apply no_adherence_tmp; auto.
   rewrite update_o. rewrite weak_update_d. apply H1. auto.
-  auto. apply sym_not_equal. apply disjoint_not_equal. auto.
+  auto. apply not_eq_sym. apply disjoint_not_equal. auto.
 Qed.
 
 Lemma weak_exec_seq_match:
diff --git a/lib/Postorder.v b/lib/Postorder.v
index 0215a829..3181c4cc 100644
--- a/lib/Postorder.v
+++ b/lib/Postorder.v
@@ -79,7 +79,7 @@ Definition transition (s: state) : PTree.t positive + state :=
       inr _ {| gr := s.(gr);
                wrk := l;
                map := PTree.set x s.(next) s.(map);
-               next := Psucc s.(next) |}
+               next := Pos.succ s.(next) |}
   | (x, y :: succs_x) :: l =>           (**r consider [y], the next unnumbered successor of [x] *)
       match s.(gr)!y with
       | None =>                         (**r [y] is already numbered: discard from worklist *)
diff --git a/lib/UnionFind.v b/lib/UnionFind.v
index 27278b01..20bb91cd 100644
--- a/lib/UnionFind.v
+++ b/lib/UnionFind.v
@@ -422,7 +422,7 @@ Definition merge (uf: t) (a b: elt) : t :=
   let b' := repr uf b in
   match M.elt_eq a' b' with
   | left EQ => uf
-  | right NEQ => identify uf a' b (repr_res_none uf a) (sym_not_equal NEQ)
+  | right NEQ => identify uf a' b (repr_res_none uf a) (not_eq_sym NEQ)
   end.
 
 Lemma repr_merge: