From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 theories/ZArith/BinInt.v       | 365 +++++++++++++++++++----------------------
 theories/ZArith/BinIntDef.v    |  10 +-
 theories/ZArith/Wf_Z.v         |  10 +-
 theories/ZArith/ZArith.v       |   2 +-
 theories/ZArith/ZArith_base.v  |   2 +-
 theories/ZArith/ZArith_dec.v   |   2 +-
 theories/ZArith/ZOdiv.v        |  88 ----------
 theories/ZArith/ZOdiv_def.v    |  15 --
 theories/ZArith/Zabs.v         |   2 +-
 theories/ZArith/Zbool.v        |   2 +-
 theories/ZArith/Zcompare.v     |   2 +-
 theories/ZArith/Zcomplements.v |  42 ++---
 theories/ZArith/Zdigits.v      |  15 +-
 theories/ZArith/Zdiv.v         |  24 ++-
 theories/ZArith/Zeuclid.v      |   2 +-
 theories/ZArith/Zeven.v        |   8 +-
 theories/ZArith/Zgcd_alt.v     |   6 +-
 theories/ZArith/Zhints.v       |   2 +-
 theories/ZArith/Zlogarithm.v   |   4 +-
 theories/ZArith/Zmax.v         |   2 +-
 theories/ZArith/Zmin.v         |   2 +-
 theories/ZArith/Zminmax.v      |   2 +-
 theories/ZArith/Zmisc.v        |   2 +-
 theories/ZArith/Znat.v         |  32 ++--
 theories/ZArith/Znumtheory.v   |  15 +-
 theories/ZArith/Zorder.v       |   2 +-
 theories/ZArith/Zpow_alt.v     |   8 +-
 theories/ZArith/Zpow_def.v     |   2 +-
 theories/ZArith/Zpow_facts.v   |   6 +-
 theories/ZArith/Zpower.v       |  26 +--
 theories/ZArith/Zquot.v        |   2 +-
 theories/ZArith/Zsqrt_compat.v |  14 +-
 theories/ZArith/Zwf.v          |   2 +-
 theories/ZArith/auxiliary.v    |   2 +-
 theories/ZArith/vo.itarget     |   2 -
 35 files changed, 290 insertions(+), 434 deletions(-)
 delete mode 100644 theories/ZArith/ZOdiv.v
 delete mode 100644 theories/ZArith/ZOdiv_def.v

(limited to 'theories/ZArith')

diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index f238ef6e..cb0c6880 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1,14 +1,14 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 Require Export BinNums BinPos Pnat.
-Require Import BinNat Bool Plus Mult Equalities GenericMinMax
+Require Import BinNat Bool Equalities GenericMinMax
  OrdersFacts ZAxioms ZProperties.
 Require BinIntDef.
 
@@ -73,6 +73,23 @@ Proof.
  decide equality; apply Pos.eq_dec.
 Defined.
 
+(** * Proofs of morphisms, obvious since eq is Leibniz *)
+
+Local Obligation Tactic := simpl_relation.
+Program Definition succ_wd : Proper (eq==>eq) succ := _.
+Program Definition pred_wd : Proper (eq==>eq) pred := _.
+Program Definition opp_wd : Proper (eq==>eq) opp := _.
+Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
+Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
+Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
+Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
+Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
+Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
+Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
+Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
+Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
+Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
+
 (** * Properties of [pos_sub] *)
 
 (** [pos_sub] can be written in term of positive comparison
@@ -138,15 +155,23 @@ Qed.
 
 Module Import Private_BootStrap.
 
-(** * Properties of addition *)
-
-(** ** Zero is neutral for addition *)
+(** ** Operations and constants *)
 
 Lemma add_0_r n : n + 0 = n.
 Proof.
  now destruct n.
 Qed.
 
+Lemma mul_0_r n : n * 0 = 0.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma mul_1_l n : 1 * n = n.
+Proof.
+ now destruct n.
+Qed.
+
 (** ** Addition is commutative *)
 
 Lemma add_comm n m : n + m = m + n.
@@ -196,28 +221,25 @@ Proof.
    symmetry. now apply Pos.add_sub_assoc.
 Qed.
 
-Lemma add_assoc n m p : n + (m + p) = n + m + p.
+Local Arguments add !x !y.
+
+Lemma add_assoc_pos p n m : pos p + (n + m) = pos p + n + m.
 Proof.
- assert (AUX : forall x y z, pos x + (y + z) = pos x + y + z).
- { intros x [|y|y] [|z|z]; rewrite ?add_0_r; trivial.
-   - simpl. now rewrite Pos.add_assoc.
-   - simpl (_ + neg _). symmetry. apply pos_sub_add.
-   - simpl (neg _ + _); simpl (_ + neg _).
-     now rewrite (add_comm _ (pos _)), <- 2 pos_sub_add, Pos.add_comm.
-   - apply opp_inj. rewrite !opp_add_distr. simpl opp.
-     simpl (neg _ + _); simpl (_ + neg _).
-     rewrite add_comm, Pos.add_comm. apply pos_sub_add. }
- destruct n.
- - trivial.
- - apply AUX.
- - apply opp_inj. rewrite !opp_add_distr. simpl opp. apply AUX.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial.
+ - now rewrite Pos.add_assoc.
+ - symmetry. apply pos_sub_add.
+ - symmetry. apply add_0_r.
+ - now rewrite <- pos_sub_add, add_comm, <- pos_sub_add, Pos.add_comm.
+ - apply opp_inj. rewrite !opp_add_distr, !pos_sub_opp.
+   rewrite add_comm, Pos.add_comm. apply pos_sub_add.
 Qed.
 
-(** ** Subtraction and successor *)
-
-Lemma sub_succ_l n m : succ n - m = succ (n - m).
+Lemma add_assoc n m p : n + (m + p) = n + m + p.
 Proof.
- unfold sub, succ. now rewrite <- 2 add_assoc, (add_comm 1).
+ destruct n.
+ - trivial.
+ - apply add_assoc_pos.
+ - apply opp_inj. rewrite !opp_add_distr. simpl. apply add_assoc_pos.
 Qed.
 
 (** ** Opposite is inverse for addition *)
@@ -227,132 +249,34 @@ Proof.
  destruct n; simpl; trivial; now rewrite pos_sub_diag.
 Qed.
 
-Lemma add_opp_diag_l n : - n + n = 0.
-Proof.
- rewrite add_comm. apply add_opp_diag_r.
-Qed.
-
-(** ** Commutativity of multiplication *)
-
-Lemma mul_comm n m : n * m = m * n.
-Proof.
- destruct n, m; simpl; trivial; f_equal; apply Pos.mul_comm.
-Qed.
-
-(** ** Associativity of multiplication *)
-
-Lemma mul_assoc n m p : n * (m * p) = n * m * p.
-Proof.
- destruct n, m, p; simpl; trivial; f_equal; apply Pos.mul_assoc.
-Qed.
-
-(** Multiplication and constants *)
-
-Lemma mul_1_l n : 1 * n = n.
-Proof.
- now destruct n.
-Qed.
-
-Lemma mul_1_r n : n * 1 = n.
-Proof.
- destruct n; simpl; now rewrite ?Pos.mul_1_r.
-Qed.
-
 (** ** Multiplication and Opposite *)
 
-Lemma mul_opp_l n m : - n * m = - (n * m).
-Proof.
- now destruct n, m.
-Qed.
-
 Lemma mul_opp_r n m : n * - m = - (n * m).
 Proof.
  now destruct n, m.
 Qed.
 
-Lemma mul_opp_opp n m : - n * - m = n * m.
-Proof.
- now destruct n, m.
-Qed.
-
-Lemma mul_opp_comm n m : - n * m = n * - m.
-Proof.
- now destruct n, m.
-Qed.
-
 (** ** Distributivity of multiplication over addition *)
 
 Lemma mul_add_distr_pos (p:positive) n m :
- pos p * (n + m) = pos p * n + pos p * m.
-Proof.
- destruct n as [|n|n], m as [|m|m]; simpl; trivial;
- rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_l; try case Pos.compare_spec;
- intros; now rewrite ?Pos.mul_add_distr_l, ?Pos.mul_sub_distr_l.
-Qed.
-
-Lemma mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
+ (n + m) * pos p = n * pos p + m * pos p.
 Proof.
- destruct n as [|n|n]. trivial.
- apply mul_add_distr_pos.
- change (neg n) with (- pos n).
- rewrite !mul_opp_l, <- opp_add_distr. f_equal.
- apply mul_add_distr_pos.
+ destruct n as [|n|n], m as [|m|m]; simpl; trivial.
+ - now rewrite Pos.mul_add_distr_r.
+ - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec;
+   simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r.
+ - rewrite ?pos_sub_spec, ?Pos.mul_compare_mono_r; case Pos.compare_spec;
+   simpl; trivial; intros; now rewrite Pos.mul_sub_distr_r.
+ - now rewrite Pos.mul_add_distr_r.
 Qed.
 
 Lemma mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
 Proof.
- rewrite !(mul_comm _ p). apply mul_add_distr_l.
-Qed.
-
-(** ** Basic properties of divisibility *)
-
-Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive.
-Proof.
- split.
- intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto.
- intros (r,H). exists (pos r); simpl; now f_equal.
-Qed.
-
-Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p).
-Proof.
- split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H.
-Qed.
-
-Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n).
-Proof.
- split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r.
-Qed.
-
-(** ** Conversions between [Z.testbit] and [N.testbit] *)
-
-Lemma testbit_of_N a n :
- testbit (of_N a) (of_N n) = N.testbit a n.
-Proof.
- destruct a as [|a], n; simpl; trivial. now destruct a.
-Qed.
-
-Lemma testbit_of_N' a n : 0<=n ->
- testbit (of_N a) n = N.testbit a (to_N n).
-Proof.
- intro Hn. rewrite <- testbit_of_N. f_equal.
- destruct n; trivial; now destruct Hn.
-Qed.
-
-Lemma testbit_Zpos a n : 0<=n ->
- testbit (pos a) n = N.testbit (N.pos a) (to_N n).
-Proof.
- intro Hn. now rewrite <- testbit_of_N'.
-Qed.
-
-Lemma testbit_Zneg a n : 0<=n ->
- testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).
-Proof.
- intro Hn.
- rewrite <- testbit_of_N' by trivial.
- destruct n as [ |n|n];
-  [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn].
- unfold testbit.
- now destruct a as [|[ | | ]| ].
+ destruct p as [|p|p].
+ - now rewrite !mul_0_r.
+ - apply mul_add_distr_pos.
+ - apply opp_inj. rewrite opp_add_distr, <- !mul_opp_r.
+   apply mul_add_distr_pos.
 Qed.
 
 End Private_BootStrap.
@@ -397,6 +321,8 @@ Qed.
 
 (** ** Specification of successor and predecessor *)
 
+Local Arguments pos_sub : simpl nomatch.
+
 Lemma succ_pred n : succ (pred n) = n.
 Proof.
  unfold succ, pred. now rewrite <- add_assoc, add_opp_diag_r, add_0_r.
@@ -511,6 +437,45 @@ Proof.
  rewrite (compare_antisym n m). case compare_spec; intuition.
 Qed.
 
+(** ** Induction principles based on successor / predecessor *)
+
+Lemma peano_ind (P : Z -> Prop) :
+  P 0 ->
+  (forall x, P x -> P (succ x)) ->
+  (forall x, P x -> P (pred x)) ->
+  forall z, P z.
+Proof.
+ intros H0 Hs Hp z; destruct z.
+ assumption.
+ induction p using Pos.peano_ind.
+  now apply (Hs 0).
+  rewrite <- Pos.add_1_r.
+  now apply (Hs (pos p)).
+ induction p using Pos.peano_ind.
+  now apply (Hp 0).
+  rewrite <- Pos.add_1_r.
+  now apply (Hp (neg p)).
+Qed.
+
+Lemma bi_induction (P : Z -> Prop) :
+  Proper (eq ==> iff) P ->
+  P 0 ->
+  (forall x, P x <-> P (succ x)) ->
+  forall z, P z.
+Proof.
+ intros _ H0 Hs. induction z using peano_ind.
+ assumption.
+ now apply -> Hs.
+ apply Hs. now rewrite succ_pred.
+Qed.
+
+(** We can now derive all properties of basic functions and orders,
+    and use these properties for proving the specs of more advanced
+    functions. *)
+
+Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+
 (** ** Specification of absolute value *)
 
 Lemma abs_eq n : 0 <= n -> abs n = n.
@@ -693,7 +658,7 @@ Lemma div_eucl_eq a b : b<>0 ->
 Proof.
  destruct a as [ |a|a], b as [ |b|b]; unfold div_eucl; trivial;
   (now destruct 1) || intros _;
-  generalize (pos_div_eucl_eq a (pos b) (eq_refl _));
+  generalize (pos_div_eucl_eq a (pos b) Logic.eq_refl);
   destruct pos_div_eucl as (q,r); rewrite mul_comm.
  - (* pos pos *)
    trivial.
@@ -756,7 +721,7 @@ Proof.
  destruct a as [|a|a]; unfold modulo, div_eucl.
  now split.
  now apply pos_div_eucl_bound.
- generalize (pos_div_eucl_bound a (pos b) (eq_refl _)).
+ generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl).
  destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
  destruct r as [|r|r]; (now destruct Hr) || clear Hr.
  now split.
@@ -773,7 +738,7 @@ Proof.
  destruct b as [|b|b]; try easy; intros _.
  destruct a as [|a|a]; unfold modulo, div_eucl.
  now split.
- generalize (pos_div_eucl_bound a (pos b) (eq_refl _)).
+ generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl).
  destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
  destruct r as [|r|r]; (now destruct Hr) || clear Hr.
  now split.
@@ -783,7 +748,7 @@ Proof.
  change (neg b - neg r <= 0). unfold le, lt in *.
   rewrite <- compare_sub. simpl in *.
   now rewrite <- Pos.compare_antisym, Hr'.
- generalize (pos_div_eucl_bound a (pos b) (eq_refl _)).
+ generalize (pos_div_eucl_bound a (pos b) Logic.eq_refl).
  destruct pos_div_eucl as (q,r); unfold snd; intros (Hr,Hr').
  split; destruct r; try easy.
   red; simpl; now rewrite <- Pos.compare_antisym.
@@ -839,6 +804,25 @@ Proof. intros _. apply rem_opp_l'. Qed.
 Lemma rem_opp_r a b : b<>0 -> rem a (-b) = rem a b.
 Proof. intros _. apply rem_opp_r'. Qed.
 
+(** ** Extra properties about [divide] *)
+
+Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive.
+Proof.
+ split.
+ intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto.
+ intros (r,H). exists (pos r); simpl; now f_equal.
+Qed.
+
+Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p).
+Proof.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H.
+Qed.
+
+Lemma divide_Zpos_Zneg_l n p : (pos p|n) <-> (neg p|n).
+Proof.
+ split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- mul_opp_r.
+Qed.
+
 (** ** Correctness proofs for gcd *)
 
 Lemma ggcd_gcd a b : fst (ggcd a b) = gcd a b.
@@ -898,6 +882,38 @@ Proof.
   destruct (Pos.ggcd a b) as (g,(aa,bb)); auto.
 Qed.
 
+(** ** Extra properties about [testbit] *)
+
+Lemma testbit_of_N a n :
+ testbit (of_N a) (of_N n) = N.testbit a n.
+Proof.
+ destruct a as [|a], n; simpl; trivial. now destruct a.
+Qed.
+
+Lemma testbit_of_N' a n : 0<=n ->
+ testbit (of_N a) n = N.testbit a (to_N n).
+Proof.
+ intro Hn. rewrite <- testbit_of_N. f_equal.
+ destruct n; trivial; now destruct Hn.
+Qed.
+
+Lemma testbit_Zpos a n : 0<=n ->
+ testbit (pos a) n = N.testbit (N.pos a) (to_N n).
+Proof.
+ intro Hn. now rewrite <- testbit_of_N'.
+Qed.
+
+Lemma testbit_Zneg a n : 0<=n ->
+ testbit (neg a) n = negb (N.testbit (Pos.pred_N a) (to_N n)).
+Proof.
+ intro Hn.
+ rewrite <- testbit_of_N' by trivial.
+ destruct n as [ |n|n];
+  [ | simpl; now destruct (Pos.pred_N a) | now destruct Hn].
+ unfold testbit.
+ now destruct a as [|[ | | ]| ].
+Qed.
+
 (** ** Proofs of specifications for bitwise operations *)
 
 Lemma div2_spec a : div2 a = shiftr a 1.
@@ -959,7 +975,7 @@ Proof.
   destruct m; easy || now destruct Hm.
  destruct a as [ |a|a].
  (* a = 0 *)
- replace (Pos.iter n div2 0) with 0
+ replace (Pos.iter div2 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
  now rewrite 2 testbit_0_l.
  (* a > 0 *)
@@ -982,7 +998,7 @@ Proof.
   rewrite ?Pos.iter_succ; apply testbit_even_0.
  destruct a as [ |a|a].
  (* a = 0 *)
- replace (Pos.iter n (mul 2) 0) with 0
+ replace (Pos.iter (mul 2) 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
  apply testbit_0_l.
  (* a > 0 *)
@@ -1013,7 +1029,7 @@ Proof.
   f_equal. now rewrite Pos.add_comm, Pos.add_sub.
  destruct a; unfold shiftl.
  (* ... a = 0 *)
- replace (Pos.iter n (mul 2) 0) with 0
+ replace (Pos.iter (mul 2) 0 n) with 0
   by (apply Pos.iter_invariant; intros; subst; trivial).
  now rewrite 2 testbit_0_l.
  (* ... a > 0 *)
@@ -1103,61 +1119,10 @@ Proof.
  now rewrite N.lxor_spec, xorb_negb_negb.
 Qed.
 
-(** ** Induction principles based on successor / predecessor *)
 
-Lemma peano_ind (P : Z -> Prop) :
-  P 0 ->
-  (forall x, P x -> P (succ x)) ->
-  (forall x, P x -> P (pred x)) ->
-  forall z, P z.
-Proof.
- intros H0 Hs Hp z; destruct z.
- assumption.
- induction p using Pos.peano_ind.
-  now apply (Hs 0).
-  rewrite <- Pos.add_1_r.
-  now apply (Hs (pos p)).
- induction p using Pos.peano_ind.
-  now apply (Hp 0).
-  rewrite <- Pos.add_1_r.
-  now apply (Hp (neg p)).
-Qed.
+(** Generic properties of advanced functions. *)
 
-Lemma bi_induction (P : Z -> Prop) :
-  Proper (eq ==> iff) P ->
-  P 0 ->
-  (forall x, P x <-> P (succ x)) ->
-  forall z, P z.
-Proof.
- intros _ H0 Hs. induction z using peano_ind.
- assumption.
- now apply -> Hs.
- apply Hs. now rewrite succ_pred.
-Qed.
-
-
-(** * Proofs of morphisms, obvious since eq is Leibniz *)
-
-Local Obligation Tactic := simpl_relation.
-Program Definition succ_wd : Proper (eq==>eq) succ := _.
-Program Definition pred_wd : Proper (eq==>eq) pred := _.
-Program Definition opp_wd : Proper (eq==>eq) opp := _.
-Program Definition add_wd : Proper (eq==>eq==>eq) add := _.
-Program Definition sub_wd : Proper (eq==>eq==>eq) sub := _.
-Program Definition mul_wd : Proper (eq==>eq==>eq) mul := _.
-Program Definition lt_wd : Proper (eq==>eq==>iff) lt := _.
-Program Definition div_wd : Proper (eq==>eq==>eq) div := _.
-Program Definition mod_wd : Proper (eq==>eq==>eq) modulo := _.
-Program Definition quot_wd : Proper (eq==>eq==>eq) quot := _.
-Program Definition rem_wd : Proper (eq==>eq==>eq) rem := _.
-Program Definition pow_wd : Proper (eq==>eq==>eq) pow := _.
-Program Definition testbit_wd : Proper (eq==>eq==>Logic.eq) testbit := _.
-
-(** The Bind Scope prevents Z to stay associated with abstract_scope.
-    (TODO FIX) *)
-
-Include ZProp. Bind Scope Z_scope with Z.
-Include UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+Include ZExtraProp.
 
 (** In generic statements, the predicates [lt] and [le] have been
   favored, whereas [gt] and [ge] don't even exist in the abstract
@@ -1277,6 +1242,8 @@ Qed.
 
 End Z.
 
+Bind Scope Z_scope with Z.t Z.
+
 (** Re-export Notations *)
 
 Infix "+" := Z.add : Z_scope.
@@ -1394,11 +1361,11 @@ Lemma inj_gcd p q : Z.pos (Pos.gcd p q) = Z.gcd (Z.pos p) (Z.pos q).
 Proof. reflexivity. Qed.
 
 Definition inj_divide p q : (Z.pos p|Z.pos q) <-> (p|q)%positive.
-Proof. apply Z.Private_BootStrap.divide_Zpos. Qed.
+Proof. apply Z.divide_Zpos. Qed.
 
 Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.pos a) n = N.testbit (N.pos a) (Z.to_N n).
-Proof. apply Z.Private_BootStrap.testbit_Zpos. Qed.
+Proof. apply Z.testbit_Zpos. Qed.
 
 (** Some results concerning Z.neg *)
 
@@ -1436,14 +1403,14 @@ Lemma add_neg_pos p q : Z.neg p + Z.pos q = Z.pos_sub q p.
 Proof. reflexivity. Qed.
 
 Lemma divide_pos_neg_r n p : (n|Z.pos p) <-> (n|Z.neg p).
-Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_r. Qed.
+Proof. apply Z.divide_Zpos_Zneg_r. Qed.
 
 Lemma divide_pos_neg_l n p : (Z.pos p|n) <-> (Z.neg p|n).
-Proof. apply Z.Private_BootStrap.divide_Zpos_Zneg_l. Qed.
+Proof. apply Z.divide_Zpos_Zneg_l. Qed.
 
 Lemma testbit_neg a n : 0<=n ->
  Z.testbit (Z.neg a) n = negb (N.testbit (Pos.pred_N a) (Z.to_N n)).
-Proof. apply Z.Private_BootStrap.testbit_Zneg. Qed.
+Proof. apply Z.testbit_Zneg. Qed.
 
 End Pos2Z.
 
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v
index 00387eec..9bb86fd5 100644
--- a/theories/ZArith/BinIntDef.v
+++ b/theories/ZArith/BinIntDef.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -126,7 +126,7 @@ Infix "*" := mul : Z_scope.
 
 (** ** Power function *)
 
-Definition pow_pos (z:Z) (n:positive) := Pos.iter n (mul z) 1.
+Definition pow_pos (z:Z) := Pos.iter (mul z) 1.
 
 Definition pow x y :=
   match y with
@@ -306,7 +306,7 @@ Definition to_pos (z:Z) : positive :=
 
 Definition iter (n:Z) {A} (f:A -> A) (x:A) :=
   match n with
-    | pos p => Pos.iter p f x
+    | pos p => Pos.iter f x p
     | _ => x
   end.
 
@@ -568,8 +568,8 @@ Definition testbit a n :=
 Definition shiftl a n :=
  match n with
    | 0 => a
-   | pos p => Pos.iter p (mul 2) a
-   | neg p => Pos.iter p div2 a
+   | pos p => Pos.iter (mul 2) a p
+   | neg p => Pos.iter div2 a p
  end.
 
 Definition shiftr a n := shiftl a (-n).
diff --git a/theories/ZArith/Wf_Z.v b/theories/ZArith/Wf_Z.v
index 5350f86d..09909bdb 100644
--- a/theories/ZArith/Wf_Z.v
+++ b/theories/ZArith/Wf_Z.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -151,9 +151,7 @@ Section Efficient_Rec.
     forall P:Z -> Prop,
       (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> 0 <= x -> P x) ->
       forall x:Z, 0 <= x -> P x.
-  Proof.
-    exact Zlt_0_rec.
-  Qed.
+  Proof. intros; now apply Zlt_0_rec. Qed.
 
   (** Obsolete version of [Z.lt] induction principle on non-negative numbers *)
 
@@ -170,7 +168,7 @@ Section Efficient_Rec.
       (forall x:Z, (forall y:Z, 0 <= y < x -> P y) -> P x) ->
       forall x:Z, 0 <= x -> P x.
   Proof.
-    exact Z_lt_rec.
+    intros; now apply Z_lt_rec.
   Qed.
 
   (** An even more general induction principle using [Z.lt]. *)
@@ -196,7 +194,7 @@ Section Efficient_Rec.
       (forall x:Z, (forall y:Z, z <= y < x -> P y) -> z <= x -> P x) ->
       forall x:Z, z <= x -> P x.
   Proof.
-    exact Zlt_lower_bound_rec.
+    intros; now apply Zlt_lower_bound_rec with z.
   Qed.
 
 End Efficient_Rec.
diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index e9cac8e1..04cccd04 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 0891c60a..4c93173b 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index e392c8b3..ac69cebd 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/ZOdiv.v b/theories/ZArith/ZOdiv.v
deleted file mode 100644
index 9fe3a365..00000000
--- a/theories/ZArith/ZOdiv.v
+++ /dev/null
@@ -1,88 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Export ZOdiv_def.
-Require Import BinInt Zquot.
-
-Notation ZO_div_mod_eq := Z.quot_rem' (only parsing).
-Notation ZOmod_lt := Zrem_lt (only parsing).
-Notation ZOmod_sgn := Zrem_sgn (only parsing).
-Notation ZOmod_sgn2 := Zrem_sgn2 (only parsing).
-Notation ZOmod_lt_pos := Zrem_lt_pos (only parsing).
-Notation ZOmod_lt_neg := Zrem_lt_neg (only parsing).
-Notation ZOmod_lt_pos_pos := Zrem_lt_pos_pos (only parsing).
-Notation ZOmod_lt_pos_neg := Zrem_lt_pos_neg (only parsing).
-Notation ZOmod_lt_neg_pos := Zrem_lt_neg_pos (only parsing).
-Notation ZOmod_lt_neg_neg := Zrem_lt_neg_neg (only parsing).
-
-Notation ZOdiv_opp_l := Zquot_opp_l (only parsing).
-Notation ZOdiv_opp_r := Zquot_opp_r (only parsing).
-Notation ZOmod_opp_l := Zrem_opp_l (only parsing).
-Notation ZOmod_opp_r := Zrem_opp_r (only parsing).
-Notation ZOdiv_opp_opp := Zquot_opp_opp (only parsing).
-Notation ZOmod_opp_opp := Zrem_opp_opp (only parsing).
-
-Notation Remainder := Remainder (only parsing).
-Notation Remainder_alt := Remainder_alt (only parsing).
-Notation Remainder_equiv := Remainder_equiv (only parsing).
-Notation ZOdiv_mod_unique_full := Zquot_mod_unique_full (only parsing).
-Notation ZOdiv_unique_full := Zquot_unique_full (only parsing).
-Notation ZOdiv_unique := Zquot_unique (only parsing).
-Notation ZOmod_unique_full := Zrem_unique_full (only parsing).
-Notation ZOmod_unique := Zrem_unique (only parsing).
-
-Notation ZOmod_0_l := Zrem_0_l (only parsing).
-Notation ZOmod_0_r := Zrem_0_r (only parsing).
-Notation ZOdiv_0_l := Zquot_0_l (only parsing).
-Notation ZOdiv_0_r := Zquot_0_r (only parsing).
-Notation ZOmod_1_r := Zrem_1_r (only parsing).
-Notation ZOdiv_1_r := Zquot_1_r (only parsing).
-Notation ZOdiv_1_l := Zquot_1_l (only parsing).
-Notation ZOmod_1_l := Zrem_1_l (only parsing).
-Notation ZO_div_same := Z_quot_same (only parsing).
-Notation ZO_mod_same := Z_rem_same (only parsing).
-Notation ZO_mod_mult := Z_rem_mult (only parsing).
-Notation ZO_div_mult := Z_quot_mult (only parsing).
-
-Notation ZO_div_pos := Z_quot_pos (only parsing).
-Notation ZO_div_lt := Z_quot_lt (only parsing).
-Notation ZOdiv_small := Zquot_small (only parsing).
-Notation ZOmod_small := Zrem_small (only parsing).
-Notation ZO_div_monotone := Z_quot_monotone (only parsing).
-Notation ZO_mult_div_le := Z_mult_quot_le (only parsing).
-Notation ZO_mult_div_ge := Z_mult_quot_ge (only parsing).
-Definition ZO_div_exact_full_1 a b := proj1 (Z_quot_exact_full a b).
-Definition ZO_div_exact_full_2 a b := proj2 (Z_quot_exact_full a b).
-Notation ZOmod_le := Zrem_le (only parsing).
-Notation ZOdiv_le_upper_bound := Zquot_le_upper_bound (only parsing).
-Notation ZOdiv_lt_upper_bound := Zquot_lt_upper_bound (only parsing).
-Notation ZOdiv_le_lower_bound := Zquot_le_lower_bound (only parsing).
-Notation ZOdiv_sgn := Zquot_sgn (only parsing).
-
-Notation ZO_mod_plus := Z_rem_plus (only parsing).
-Notation ZO_div_plus := Z_quot_plus (only parsing).
-Notation ZO_div_plus_l := Z_quot_plus_l (only parsing).
-Notation ZOdiv_mult_cancel_r := Zquot_mult_cancel_r (only parsing).
-Notation ZOdiv_mult_cancel_l := Zquot_mult_cancel_l (only parsing).
-Notation ZOmult_mod_distr_l := Zmult_rem_distr_l (only parsing).
-Notation ZOmult_mod_distr_r := Zmult_rem_distr_r (only parsing).
-Notation ZOmod_mod := Zrem_rem (only parsing).
-Notation ZOmult_mod := Zmult_rem (only parsing).
-Notation ZOplus_mod := Zplus_rem (only parsing).
-Notation ZOplus_mod_idemp_l := Zplus_rem_idemp_l (only parsing).
-Notation ZOplus_mod_idemp_r := Zplus_rem_idemp_r (only parsing).
-Notation ZOmult_mod_idemp_l := Zmult_rem_idemp_l (only parsing).
-Notation ZOmult_mod_idemp_r := Zmult_rem_idemp_r (only parsing).
-Notation ZOdiv_ZOdiv := Zquot_Zquot (only parsing).
-Notation ZOdiv_mult_le := Zquot_mult_le (only parsing).
-Notation ZOmod_divides := Zrem_divides (only parsing).
-
-Notation ZOdiv_eucl_Zdiv_eucl_pos := Zquotrem_Zdiv_eucl_pos (only parsing).
-Notation ZOdiv_Zdiv_pos := Zquot_Zdiv_pos (only parsing).
-Notation ZOmod_Zmod_pos := Zrem_Zmod_pos (only parsing).
-Notation ZOmod_Zmod_zero := Zrem_Zmod_zero (only parsing).
diff --git a/theories/ZArith/ZOdiv_def.v b/theories/ZArith/ZOdiv_def.v
deleted file mode 100644
index 8b823d9f..00000000
--- a/theories/ZArith/ZOdiv_def.v
+++ /dev/null
@@ -1,15 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-Require Import BinInt.
-
-Notation ZOdiv_eucl := Z.quotrem (only parsing).
-Notation ZOdiv := Z.quot (only parsing).
-Notation ZOmod := Z.rem (only parsing).
-
-Notation ZOdiv_eucl_correct := Z.quotrem_eq.
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index aa3d1188..146009bc 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zbool.v b/theories/ZArith/Zbool.v
index 81e52728..61eb2a34 100644
--- a/theories/ZArith/Zbool.v
+++ b/theories/ZArith/Zbool.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zcompare.v b/theories/ZArith/Zcompare.v
index 6aa26d19..d4ac72e9 100644
--- a/theories/ZArith/Zcompare.v
+++ b/theories/ZArith/Zcompare.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index dceac4f2..9604a06e 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -53,17 +53,18 @@ Theorem Z_lt_abs_rec :
     forall n:Z, P n.
 Proof.
   intros P HP p.
-  set (Q := fun z => 0 <= z -> P z * P (- z)) in *.
-  cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ].
-  elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
-  unfold Q; clear Q; intros.
+  set (Q := fun z => 0 <= z -> P z * P (- z)).
+  enough (H:Q (Z.abs p)) by
+    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
+  apply (Z_lt_rec Q); auto with zarith.
+  subst Q; intros x H.
   split; apply HP.
-  rewrite Z.abs_eq; auto; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
-  rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  - rewrite Z.abs_eq; auto; intros.
+    destruct (H (Z.abs m)); auto with zarith.
+    destruct (Zabs_dec m) as [-> | ->]; trivial.
+  - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
+    destruct (H (Z.abs m)); auto with zarith.
+    destruct (Zabs_dec m) as [-> | ->]; trivial.
 Qed.
 
 Theorem Z_lt_abs_induction :
@@ -73,16 +74,17 @@ Theorem Z_lt_abs_induction :
 Proof.
   intros P HP p.
   set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *.
-  cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ].
-  elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith.
-  unfold Q; clear Q; intros.
+  enough (Q (Z.abs p)) by
+    (destruct (Zabs_dec p) as [-> | ->]; elim H; auto with zarith).
+  apply (Z_lt_induction Q); auto with zarith.
+  subst Q; intros.
   split; apply HP.
-  rewrite Z.abs_eq; auto; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
-  rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
-  elim (H (Z.abs m)); intros; auto with zarith.
-  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  - rewrite Z.abs_eq; auto; intros.
+    elim (H (Z.abs m)); intros; auto with zarith.
+    elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  - rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros.
+    destruct (H (Z.abs m)); auto with zarith.
+    destruct (Zabs_dec m) as [-> | ->]; trivial.
 Qed.
 
 (** To do case analysis over the sign of [z] *)
diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index bf19c8ec..b5d04719 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -41,7 +41,7 @@ Section VALUE_OF_BOOLEAN_VECTORS.
 
   Lemma binary_value : forall n:nat, Bvector n -> Z.
   Proof.
-    simple induction n; intros.
+    refine (nat_rect _ _ _); intros.
     exact 0%Z.
 
     inversion H0.
@@ -152,7 +152,7 @@ Section Z_BRIC_A_BRAC.
   Lemma binary_value_pos :
     forall (n:nat) (bv:Bvector n), (binary_value n bv >= 0)%Z.
   Proof.
-    induction bv as [| a n v IHbv]; simpl.
+    induction bv as [| a n v IHbv]; cbn.
     omega.
 
     destruct a; destruct (binary_value n v); simpl; auto.
@@ -212,14 +212,11 @@ Section Z_BRIC_A_BRAC.
       (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z.
   Proof.
     intros.
-    cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros.
-    omega.
-
+    enough (2 * Z.div2 z < 2 * two_power_nat n)%Z by omega.
     rewrite <- two_power_nat_S.
-    destruct (Zeven.Zeven_odd_dec z); intros.
+    destruct (Zeven.Zeven_odd_dec z) as [Heven|Hodd]; intros.
     rewrite <- Zeven.Zeven_div2; auto.
-
-    generalize (Zeven.Zodd_div2 z z0); omega.
+    generalize (Zeven.Zodd_div2 z Hodd); omega.
   Qed.
 
   Lemma Z_to_two_compl_Sn_z :
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 2e3a2280..d0d10891 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -666,24 +666,22 @@ Theorem Zdiv_eucl_extended :
       {qr : Z * Z | let (q, r) := qr in a = b * q + r /\ 0 <= r < Z.abs b}.
 Proof.
   intros b Hb a.
-  elim (Z_le_gt_dec 0 b); intro Hb'.
-  cut (b > 0); [ intro Hb'' | omega ].
-  rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
-  cut (- b > 0); [ intro Hb'' | omega ].
-  elim (Zdiv_eucl_exist Hb'' a); intros qr.
-  elim qr; intros q r Hqr.
-  exists (- q, r).
-  elim Hqr; intros.
-  split.
-  rewrite <- Z.mul_opp_comm; assumption.
-  rewrite Z.abs_neq; [ assumption | omega ].
+  destruct (Z_le_gt_dec 0 b) as [Hb'|Hb'].
+  - assert (Hb'' : b > 0) by omega.
+    rewrite Z.abs_eq; [ apply Zdiv_eucl_exist; assumption | assumption ].
+  - assert (Hb'' : - b > 0) by omega.
+    destruct (Zdiv_eucl_exist Hb'' a) as ((q,r),[]).
+    exists (- q, r).
+    split.
+    + rewrite <- Z.mul_opp_comm; assumption.
+    + rewrite Z.abs_neq; [ assumption | omega ].
 Qed.
 
 Arguments Zdiv_eucl_extended : default implicits.
 
 (** * Division and modulo in Z agree with same in nat: *)
 
-Require Import NPeano.
+Require Import PeanoNat.
 
 Lemma div_Zdiv (n m: nat): m <> O ->
   Z.of_nat (n / m) = Z.of_nat n / Z.of_nat m.
diff --git a/theories/ZArith/Zeuclid.v b/theories/ZArith/Zeuclid.v
index 39e846a0..f5cacc7e 100644
--- a/theories/ZArith/Zeuclid.v
+++ b/theories/ZArith/Zeuclid.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zeven.v b/theories/ZArith/Zeven.v
index c83a863f..d88bf7a9 100644
--- a/theories/ZArith/Zeven.v
+++ b/theories/ZArith/Zeven.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -197,12 +197,14 @@ Qed.
 Lemma Zquot2_quot n : Z.quot2 n = n ÷ 2.
 Proof.
  assert (AUX : forall m, 0 < m -> Z.quot2 m = m ÷ 2).
- { intros m Hm.
+  {
+   intros m Hm.
    apply Z.quot_unique with (if Z.odd m then Z.sgn m else 0).
    now apply Z.lt_le_incl.
    rewrite Z.sgn_pos by trivial.
    destruct (Z.odd m); now split.
-   apply Zquot2_odd_eqn. }
+   apply Zquot2_odd_eqn.
+  }
  destruct (Z.lt_trichotomy 0 n) as [POS|[NUL|NEG]].
  - now apply AUX.
  - now subst.
diff --git a/theories/ZArith/Zgcd_alt.v b/theories/ZArith/Zgcd_alt.v
index 1e19479e..14286bde 100644
--- a/theories/ZArith/Zgcd_alt.v
+++ b/theories/ZArith/Zgcd_alt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -23,6 +23,7 @@ Require Import ZArith_base.
 Require Import ZArithRing.
 Require Import Zdiv.
 Require Import Znumtheory.
+Require Import Omega.
 
 Open Scope Z_scope.
 
@@ -104,8 +105,7 @@ Open Scope Z_scope.
 
  Lemma fibonacci_pos : forall n, 0 <= fibonacci n.
  Proof.
-   cut (forall N n, (n<N)%nat -> 0<=fibonacci n).
-   eauto.
+   enough (forall N n, (n<N)%nat -> 0<=fibonacci n) by eauto.
    induction N.
    inversion 1.
    intros.
diff --git a/theories/ZArith/Zhints.v b/theories/ZArith/Zhints.v
index 411fec67..1942c2ab 100644
--- a/theories/ZArith/Zhints.v
+++ b/theories/ZArith/Zhints.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 59c16469..6e349569 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -59,7 +59,7 @@ Section Log_pos. (* Log of positive integers *)
 
   Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p.
   Proof.
-   induction p; simpl.
+   induction p; simpl log_sup.
    - change (Zpos p~1) with (2*(Zpos p)+1).
      rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy.
      unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc.
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index 78091794..c436b3ad 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 98282b38..1cfa2e03 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zminmax.v b/theories/ZArith/Zminmax.v
index d3376a0e..05a94a8e 100644
--- a/theories/ZArith/Zminmax.v
+++ b/theories/ZArith/Zminmax.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zmisc.v b/theories/ZArith/Zmisc.v
index 203f9766..b401e6b6 100644
--- a/theories/ZArith/Zmisc.v
+++ b/theories/ZArith/Zmisc.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 8031b357..20e7c2e8 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -271,7 +271,7 @@ Qed.
 
 Lemma inj_testbit a n :
  Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n.
-Proof. apply Z.Private_BootStrap.testbit_of_N. Qed.
+Proof. apply Z.testbit_of_N. Qed.
 
 End N2Z.
 
@@ -426,7 +426,7 @@ Qed.
 
 Lemma inj_testbit a n : 0<=n ->
  Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n).
-Proof. apply Z.Private_BootStrap.testbit_of_N'. Qed.
+Proof. apply Z.testbit_of_N'. Qed.
 
 End Z2N.
 
@@ -637,7 +637,7 @@ Qed.
 
 (** [Z.of_nat] and usual operations *)
 
-Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = nat_compare n m.
+Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = (n ?= m)%nat.
 Proof.
  now rewrite <-!nat_N_Z, N2Z.inj_compare, <- Nat2N.inj_compare.
 Qed.
@@ -690,23 +690,23 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub.
 Qed.
 
-Lemma inj_pred_max n : Z.of_nat (pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
+Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max.
 Qed.
 
-Lemma inj_pred n : (0<n)%nat -> Z.of_nat (pred n) = Z.pred (Z.of_nat n).
+Lemma inj_pred n : (0<n)%nat -> Z.of_nat (Nat.pred n) = Z.pred (Z.of_nat n).
 Proof.
  rewrite nat_compare_lt, Nat2N.inj_compare. intros.
  now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred.
 Qed.
 
-Lemma inj_min n m : Z.of_nat (min n m) = Z.min (Z.of_nat n) (Z.of_nat m).
+Lemma inj_min n m : Z.of_nat (Nat.min n m) = Z.min (Z.of_nat n) (Z.of_nat m).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_min, N2Z.inj_min.
 Qed.
 
-Lemma inj_max n m : Z.of_nat (max n m) = Z.max (Z.of_nat n) (Z.of_nat m).
+Lemma inj_max n m : Z.of_nat (Nat.max n m) = Z.max (Z.of_nat n) (Z.of_nat m).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_max, N2Z.inj_max.
 Qed.
@@ -777,13 +777,13 @@ Proof.
  intros. now rewrite <- !Z_N_nat, Z2N.inj_sub, N2Nat.inj_sub.
 Qed.
 
-Lemma inj_pred n : Z.to_nat (Z.pred n) = pred (Z.to_nat n).
+Lemma inj_pred n : Z.to_nat (Z.pred n) = Nat.pred (Z.to_nat n).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_pred, N2Nat.inj_pred.
 Qed.
 
 Lemma inj_compare n m : 0<=n -> 0<=m ->
- nat_compare (Z.to_nat n) (Z.to_nat m) = (n ?= m).
+ (Z.to_nat n ?= Z.to_nat m)%nat = (n ?= m).
 Proof.
  intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id.
 Qed.
@@ -798,12 +798,12 @@ Proof.
  intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare.
 Qed.
 
-Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m).
+Lemma inj_min n m : Z.to_nat (Z.min n m) = Nat.min (Z.to_nat n) (Z.to_nat m).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min.
 Qed.
 
-Lemma inj_max n m : Z.to_nat (Z.max n m) = max (Z.to_nat n) (Z.to_nat m).
+Lemma inj_max n m : Z.to_nat (Z.max n m) = Nat.max (Z.to_nat n) (Z.to_nat m).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_max, N2Nat.inj_max.
 Qed.
@@ -876,13 +876,13 @@ Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_sub, N2Nat.inj_sub.
 Qed.
 
-Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = pred (Z.abs_nat n).
+Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = Nat.pred (Z.abs_nat n).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_pred, N2Nat.inj_pred.
 Qed.
 
 Lemma inj_compare n m : 0<=n -> 0<=m ->
- nat_compare (Z.abs_nat n) (Z.abs_nat m) = (n ?= m).
+ (Z.abs_nat n ?= Z.abs_nat m)%nat = (n ?= m).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare.
 Qed.
@@ -898,13 +898,13 @@ Proof.
 Qed.
 
 Lemma inj_min n m : 0<=n -> 0<=m ->
- Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m).
+ Z.abs_nat (Z.min n m) = Nat.min (Z.abs_nat n) (Z.abs_nat m).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_min, N2Nat.inj_min.
 Qed.
 
 Lemma inj_max n m : 0<=n -> 0<=m ->
- Z.abs_nat (Z.max n m) = max (Z.abs_nat n) (Z.abs_nat m).
+ Z.abs_nat (Z.max n m) = Nat.max (Z.abs_nat n) (Z.abs_nat m).
 Proof.
  intros. now rewrite <- !Zabs_N_nat, Zabs2N.inj_max, N2Nat.inj_max.
 Qed.
diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v
index 0f58f524..f69cf315 100644
--- a/theories/ZArith/Znumtheory.v
+++ b/theories/ZArith/Znumtheory.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -308,11 +308,11 @@ Section extended_euclid_algorithm.
     intros v3 Hv3; generalize Hv3; pattern v3.
     apply Zlt_0_rec.
     clear v3 Hv3; intros.
-    elim (Z_zerop x); intro.
+    destruct (Z_zerop x) as [Heq|Hneq].
     apply Euclid_intro with (u := u1) (v := u2) (d := u3).
     assumption.
     apply H3.
-    rewrite a0; auto with zarith.
+    rewrite Heq; auto with zarith.
     set (q := u3 / x) in *.
     assert (Hq : 0 <= u3 - q * x < x).
     replace (u3 - q * x) with (u3 mod x).
@@ -605,11 +605,10 @@ Qed.
 Lemma prime_rel_prime :
   forall p:Z, prime p -> forall a:Z, ~ (p | a) -> rel_prime p a.
 Proof.
-  simple induction 1; intros.
-  constructor; intuition.
-  elim (prime_divisors p H x H3); intuition; subst; auto with zarith.
-  absurd (p | a); auto with zarith.
-  absurd (p | a); intuition.
+  intros; constructor; intros; auto with zarith.
+  apply prime_divisors in H1; intuition; subst; auto with zarith.
+  - absurd (p | a); auto with zarith.
+  - absurd (p | a); intuition.
 Qed.
 
 Hint Resolve prime_rel_prime: zarith.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 39cf87fa..e090302e 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zpow_alt.v b/theories/ZArith/Zpow_alt.v
index a35dcb68..8f661a9c 100644
--- a/theories/ZArith/Zpow_alt.v
+++ b/theories/ZArith/Zpow_alt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -30,12 +30,12 @@ Infix "^^" := Zpower_alt (at level 30, right associativity) : Z_scope.
 
 Lemma Piter_mul_acc : forall f,
  (forall x y:Z, (f x)*y = f (x*y)) ->
- forall p k, Pos.iter p f k = (Pos.iter p f 1)*k.
+ forall p k, Pos.iter f k p = (Pos.iter f 1 p)*k.
 Proof.
  intros f Hf.
  induction p; simpl; intros.
- - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Hf, Z.mul_assoc.
- - set (g := Pos.iter p f 1) in *. now rewrite !IHp, Z.mul_assoc.
+ - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Hf, Z.mul_assoc.
+ - set (g := Pos.iter f 1 p) in *. now rewrite !IHp, Z.mul_assoc.
  - now rewrite Hf, Z.mul_1_l.
 Qed.
 
diff --git a/theories/ZArith/Zpow_def.v b/theories/ZArith/Zpow_def.v
index 2fbb70ba..740c45fd 100644
--- a/theories/ZArith/Zpow_def.v
+++ b/theories/ZArith/Zpow_def.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zpow_facts.v b/theories/ZArith/Zpow_facts.v
index 86dfce16..ac41a98f 100644
--- a/theories/ZArith/Zpow_facts.v
+++ b/theories/ZArith/Zpow_facts.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -152,10 +152,8 @@ Qed.
 Theorem Zpow_mod_correct a m n :
  n <> 0 -> Zpow_mod a m n = (a ^ m) mod n.
 Proof.
-  intros Hn. destruct m; simpl.
-  - trivial.
+  intros Hn. destruct m; simpl; trivial.
   - apply Zpow_mod_pos_correct; auto with zarith.
-  - rewrite Z.mod_0_l; auto with zarith.
 Qed.
 
 (* Complements about power and number theory. *)
diff --git a/theories/ZArith/Zpower.v b/theories/ZArith/Zpower.v
index 27f0cfd2..747bd4fd 100644
--- a/theories/ZArith/Zpower.v
+++ b/theories/ZArith/Zpower.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -25,7 +25,7 @@ Local Open Scope Z_scope.
 (** [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
     integer (type [nat]) and [z] a signed integer (type [Z]) *)
 
-Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1.
+Definition Zpower_nat (z:Z) := nat_rect _ 1 (fun _ => Z.mul z).
 
 Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.
 Proof. reflexivity. Qed.
@@ -42,7 +42,7 @@ Lemma Zpower_nat_is_exp :
 Proof.
  induction n.
  - intros. now rewrite Zpower_nat_0_r, Z.mul_1_l.
- - intros. simpl. now rewrite 2 Zpower_nat_succ_r, IHn, Z.mul_assoc.
+ - intros. simpl. now rewrite IHn, Z.mul_assoc.
 Qed.
 
 (** Conversions between powers of unary and binary integers *)
@@ -94,12 +94,12 @@ Section Powers_of_2.
       calculus is possible. [shift n m] computes [2^n * m], i.e.
       [m] shifted by [n] positions *)
 
-  Definition shift_nat (n:nat) (z:positive) := nat_iter n xO z.
-  Definition shift_pos (n z:positive) := Pos.iter n xO z.
+  Definition shift_nat (n:nat) (z:positive) := nat_rect _ z (fun _ => xO) n.
+  Definition shift_pos (n z:positive) := Pos.iter xO z n.
   Definition shift (n:Z) (z:positive) :=
     match n with
       | Z0 => z
-      | Zpos p => Pos.iter p xO z
+      | Zpos p => Pos.iter xO z p
       | Zneg p => z
     end.
 
@@ -154,7 +154,7 @@ Section Powers_of_2.
   Lemma shift_nat_plus n m x :
     shift_nat (n + m) x = shift_nat n (shift_nat m x).
   Proof.
-   apply iter_nat_plus.
+   induction n; simpl; now f_equal.
   Qed.
 
   Theorem shift_nat_correct n x :
@@ -247,20 +247,20 @@ Section power_div_with_rest.
        end, 2 * d).
 
   Definition Zdiv_rest (x:Z) (p:positive) :=
-    let (qr, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in qr.
+    let (qr, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in qr.
 
   Lemma Zdiv_rest_correct1 (x:Z) (p:positive) :
-    let (_, d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+    let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
     d = two_power_pos p.
   Proof.
    rewrite Pos2Nat.inj_iter, two_power_pos_nat.
    induction (Pos.to_nat p); simpl; trivial.
-   destruct (nat_iter n Zdiv_rest_aux (x,0,1)) as ((q,r),d).
+   destruct (nat_rect _ _ _ _) as ((q,r),d).
    unfold Zdiv_rest_aux. rewrite two_power_nat_S; now f_equal.
   Qed.
 
   Lemma Zdiv_rest_correct2 (x:Z) (p:positive) :
-    let '(q,r,d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) in
+    let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
     x = q * d + r /\ 0 <= r < d.
   Proof.
    apply Pos.iter_invariant; [|omega].
@@ -287,7 +287,7 @@ Section power_div_with_rest.
   Lemma Zdiv_rest_correct (x:Z) (p:positive) : Zdiv_rest_proofs x p.
   Proof.
     generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-    destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+    destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d).
     intros (H1,(H2,H3)) ->. now exists q r.
   Qed.
 
@@ -299,7 +299,7 @@ Section power_div_with_rest.
   Proof.
    unfold Zdiv_rest.
    generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).
-   destruct (Pos.iter p Zdiv_rest_aux (x, 0, 1)) as ((q,r),d).
+   destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d).
    intros H ->. now rewrite two_power_pos_equiv in H.
   Qed.
 
diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v
index 7f064c2b..3ef11189 100644
--- a/theories/ZArith/Zquot.v
+++ b/theories/ZArith/Zquot.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index 24f3715e..65959a69 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -53,7 +53,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
 	| xI xH => c_sqrt 3 1 2 _ _
 	| xO (xO p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r') with
 		| left Hle =>
                   c_sqrt (Zpos (xO (xO p'))) (2 * s' + 1)
@@ -63,7 +63,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
           end
 	| xO (xI p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r' + 2) with
 		| left Hle =>
                   c_sqrt (Zpos (xO (xI p'))) (2 * s' + 1)
@@ -74,7 +74,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
           end
 	| xI (xO p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r' + 1) with
 		| left Hle =>
                   c_sqrt (Zpos (xI (xO p'))) (2 * s' + 1)
@@ -85,7 +85,7 @@ Definition sqrtrempos : forall p:positive, sqrt_data (Zpos p).
           end
 	| xI (xI p') =>
           match sqrtrempos p' with
-            | c_sqrt s' r' Heq Hint =>
+            | c_sqrt _ s' r' Heq Hint =>
               match Z_le_gt_dec (4 * s' + 1) (4 * r' + 3) with
 		| left Hle =>
                   c_sqrt (Zpos (xI (xI p'))) (2 * s' + 1)
@@ -114,7 +114,7 @@ Definition Zsqrt :
 	| Zpos p =>
           fun h =>
             match sqrtrempos p with
-              | c_sqrt s r Heq Hint =>
+              | c_sqrt _ s r Heq Hint =>
 		existT
                 (fun s:Z =>
                   {r : Z |
@@ -150,7 +150,7 @@ Definition Zsqrt_plain (x:Z) : Z :=
   match x with
     | Zpos p =>
       match Zsqrt (Zpos p) (Pos2Z.is_nonneg p) with
-	| existT s _ => s
+	| existT _ s _ => s
       end
     | Zneg p => 0
     | Z0 => 0
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 9d2e9cab..cba709e8 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 929aedc9..25ef852a 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -1,7 +1,7 @@
 (* -*- coding: utf-8 -*- *)
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 88751cc0..178111cd 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -23,8 +23,6 @@ Zmin.vo
 Zmisc.vo
 Znat.vo
 Znumtheory.vo
-ZOdiv_def.vo
-ZOdiv.vo
 Zquot.vo
 Zorder.vo
 Zpow_def.vo
-- 
cgit v1.2.3