Update the -compat flags

Mostly via `dev/tools/update-compat.py --cur-version=8.9`

We just remove test-suite/success/FunindExtraction_compat86.v because,
except for the `Extraction iszero.` line at the bottom, it is a
duplicate of `test-suite/success/Funind.v` (except with `-compat 8.6`).

We also manually update a number of test-suite files to pre-emptively
remove compatibility notations (which used to be compat 8.6, but are now
compat 8.7).

22 files changed, 450 insertions, 968 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 0fa42cadad..4cbf75b715 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -600,8 +600,8 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq86.v
     theories/Compat/Coq87.v
     theories/Compat/Coq88.v
+    theories/Compat/Coq89.v
   </dd>
 </dl>
diff --git a/lib/flags.ml b/lib/flags.ml
index 4d6c36f55d..c8f19f2f11 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -66,25 +66,25 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-  | V8_6, V8_6 -> 0
-  | V8_6, _ -> -1
-  | _, V8_6 -> 1
   | V8_7, V8_7 -> 0
   | V8_7, _ -> -1
   | _, V8_7 -> 1
+  | V8_8, V8_8 -> 0
+  | V8_8, _ -> -1
+  | _, V8_8 -> 1
   | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
-  | V8_6 -> "8.6"
   | V8_7 -> "8.7"
+  | V8_8 -> "8.8"
   | Current -> "current"
 
 (* Translate *)
diff --git a/lib/flags.mli b/lib/flags.mli
index 398f22ab4f..3d9eafde75 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -58,7 +58,7 @@ val we_are_parsing : bool ref
 (* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
 
-type compat_version = V8_6 | V8_7 | Current
+type compat_version = V8_7 | V8_8 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 162adf0626..d86c094b1f 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -795,9 +795,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
 	  | [], [] -> []
 	  | _ -> assert false
 	in aux 1 1 (List.rev nal) cs.cs_args, true in
-    let fsign = if Flags.version_strictly_greater Flags.V8_6
-                then Context.Rel.map (whd_betaiota !evdref) fsign
-                else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+    let fsign = Context.Rel.map (whd_betaiota !evdref) fsign in
     let fsign,env_f = push_rel_context !evdref fsign env in
     let obj ind p v f =
       if not record then
@@ -896,10 +894,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
-        let cs_args =
-          if Flags.version_strictly_greater Flags.V8_6
-          then Context.Rel.map (whd_betaiota !evdref) cs_args
-          else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
+        let cs_args = Context.Rel.map (whd_betaiota !evdref) cs_args in
 	let csgn =
           List.map (set_name Anonymous) cs_args
         in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e223674579..4665486fc0 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -193,10 +193,7 @@ let pose_all_metas_as_evars env evd t =
        | None ->
         let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
-        let ty =
-          if Flags.version_strictly_greater Flags.V8_6
-          then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
-          else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
+        let ty = nf_betaiota env evd ty in
         let src = Evd.evar_source_of_meta mv !evdref in
         let evd, ev = Evarutil.new_evar env !evdref ~src ty in
         evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
diff --git a/test-suite/bugs/closed/2378.v b/test-suite/bugs/closed/2378.v
index 6d73d58d4e..b9dd654057 100644
--- a/test-suite/bugs/closed/2378.v
+++ b/test-suite/bugs/closed/2378.v
@@ -73,7 +73,7 @@ Fixpoint LPTransfo Pred1 Pred2 p2lp (f: LP Pred1): LP Pred2 :=
   end.
 Arguments LPTransfo : default implicits.
 
-Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f := 
+Definition addIndex (Ind:Type) (Pred: Ind -> Type) (i: Ind) f :=
   LPTransfo (fun p => LPPred _ (existT (fun i => Pred i) i p)) f.
 
 Section TTS.
@@ -121,8 +121,8 @@ Record simu (Pred: Type) (a: TTS StateA) (c: TTS StateC) (tra: Pred -> LP (Predi
     Delay _ a (mabs m ex1 st1) d (mabs m (mDelay m ex1 st1 d) st2);
   simuNext: forall ex1 st1 st2, Next _ c st1 st2 -> inv ex1 st1 ->
     Next _ a (mabs m ex1 st1) (mabs m (mNext m ex1 st1) st2);
-  simuPred: forall ext st, inv ext st -> 
-    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p)) 
+  simuPred: forall ext st, inv ext st ->
+    (forall p, lpSat (Satisfy _ c) st (trc p) <-> lpSat (Satisfy _ a) (mabs m ext st) (tra p))
 }.
 
 Theorem satProd: forall State Ind Pred (Sat: forall i, State -> Pred i -> Prop) (st:State) i (f: LP (Pred i)),
@@ -137,15 +137,15 @@ Qed.
 
 Definition trProd (State: Type) Ind (Pred: Ind -> Type) (tts: Ind -> TTS State) (tr: forall i, (Pred i) -> LP (Predicate _ (tts i))):
   {i:Ind & Pred i} -> LP (Predicate _ (TTSIndexedProduct _ Ind tts)) :=
-  fun p => addIndex Ind _ (projS1 p) (tr (projS1 p) (projS2 p)).
+  fun p => addIndex Ind _ (projT1 p) (tr (projT1 p) (projT2 p)).
 
 Arguments trProd : default implicits.
 Require Import Setoid.
 
 Theorem satTrProd:
-  forall State Ind Pred (tts: Ind -> TTS State) 
+  forall State Ind Pred (tts: Ind -> TTS State)
     (tr: forall i, (Pred  i) -> LP (Predicate _ (tts i))) (st:State) (p: {i:Ind & (Pred i)}),
-  lpSat (Satisfy _ (tts (projS1 p))) st (tr (projS1 p) (projS2 p))
+  lpSat (Satisfy _ (tts (projT1 p))) st (tr (projT1 p) (projT2 p))
   <->
   lpSat (Satisfy _ (TTSIndexedProduct _ _ tts)) st (trProd _ tts tr p).
 Proof.
@@ -154,11 +154,11 @@ Proof.
                       (fun i => Satisfy _ (tts i))); tauto.
 Qed.
 
-Theorem simuProd: 
-  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+Theorem simuProd:
+  forall Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC)
     (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
     (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
-     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) -> 
+     (forall i, simu _ (tta i) (ttc i) (tra i) (trc i)) ->
        simu _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
                   (trProd Pred tta tra) (trProd Pred ttc trc).
 Proof.
@@ -171,11 +171,11 @@ Proof.
   eapply simuDelay; eauto.
   eapply simuNext; eauto.
   split; simpl; intros.
-  generalize (proj1 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  generalize (proj1 (simuPred _ _ _ _ _ (X (projT1 p)) ext st (H (projT1 p)) (projT2 p))); simpl; intro.
   rewrite <- (satTrProd StateA Ind Pred tta tra); apply H1.
   rewrite (satTrProd StateC Ind Pred ttc trc); apply H0.
 
-  generalize (proj2 (simuPred _ _ _ _ _ (X (projS1 p)) ext st (H (projS1 p)) (projS2 p))); simpl; intro.
+  generalize (proj2 (simuPred _ _ _ _ _ (X (projT1 p)) ext st (H (projT1 p)) (projT2 p))); simpl; intro.
   rewrite <- (satTrProd StateC Ind Pred ttc trc); apply H1.
   rewrite (satTrProd StateA Ind Pred tta tra); apply H0.
 Qed.
@@ -189,11 +189,11 @@ Record simu_equiv StateA StateC m1 m2 Pred (a: TTS StateA) (c: TTS StateC) (tra:
   simuRL: simu StateC StateA m2 Pred c a trc tra
 }.
 
-Theorem simu_equivProd: 
-  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC) 
+Theorem simu_equivProd:
+  forall StateA StateC m1 m2 Ind (Pred: Ind -> Type) (tta: Ind -> TTS StateA) (ttc: Ind -> TTS StateC)
     (tra: forall i, (Pred i) -> LP (Predicate _ (tta i)))
     (trc: forall i, (Pred i) -> LP (Predicate _ (ttc i))),
-     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) -> 
+     (forall i, simu_equiv StateA StateC m1 m2 _ (tta i) (ttc i) (tra i) (trc i)) ->
        simu_equiv StateA StateC m1 m2 _ (TTSIndexedProduct _ Ind tta) (TTSIndexedProduct _ Ind ttc)
                   (trProd _ _ Pred tta tra) (trProd _ _ Pred ttc trc).
 Proof.
@@ -237,7 +237,7 @@ Definition pPredicate (L: RTLanguage) (sys: PSyntax L) := { i : pIndex L sys & M
 
 (* product with shared state *)
 
-Definition PLanguage (L: RTLanguage): RTLanguage := 
+Definition PLanguage (L: RTLanguage): RTLanguage :=
   mkRTLanguage
     (PSyntax L)
     (pState L)
@@ -246,7 +246,7 @@ Definition PLanguage (L: RTLanguage): RTLanguage :=
         eq_refl => Semantic L (pComponents L mdl i)
        end))
     (pPredicate L)
-    (fun mdl => trProd _ _ _ _ 
+    (fun mdl => trProd _ _ _ _
       (fun i pi => match pIsShared L mdl i as e in (_ = y) return
                      (LP (Predicate y
                                match e in (_ = y0) return (TTS y0) with
@@ -259,22 +259,22 @@ Definition PLanguage (L: RTLanguage): RTLanguage :=
 Inductive Empty: Type :=.
 
 Record isSharedTransfo l1 l2 tr: Prop := isSharedTransfoPrf {
-sameState:  forall mdl i j, 
+sameState:  forall mdl i j,
   DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i)) =
   DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl j));
-sameMState: forall mdl i j, 
+sameMState: forall mdl i j,
   mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl i)) =
   mState _ _  (Tl1l2 _ _ tr (pComponents l1 mdl j));
-sameM12: forall mdl i j, 
+sameM12: forall mdl i j,
   Tl1l2 _ _ tr (pComponents l1 mdl i) =
   match sym_eq (sameState mdl i j) in _=y return mapping _ y with
     eq_refl => match sym_eq (pIsShared l1 mdl i) in _=x return mapping x _ with
       eq_refl => match pIsShared l1 mdl j in _=x return mapping x _ with
         eq_refl => Tl1l2 _ _ tr (pComponents l1 mdl j)
       end
-    end         
+    end
   end;
-sameM21: forall mdl i j, 
+sameM21: forall mdl i j,
   Tl2l1 l1 l2 tr (pComponents l1 mdl i) =
   match
     sym_eq (sameState mdl i j) in (_ = y)
@@ -301,7 +301,7 @@ end
 Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
   mkPSyntax l2 (pIndex l1 mdl)
     (pIsEmpty l1 mdl)
-    (match pIsEmpty l1 mdl return Type with 
+    (match pIsEmpty l1 mdl return Type with
          inleft i => DynamicState l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))
         |inright h => pState l1 mdl
        end)
@@ -314,7 +314,7 @@ Definition PTransfoSyntax l1 l2 tr (h: isSharedTransfo l1 l2 tr) mdl :=
          | inright _ => pState l1 mdl
          end)
       with
-         inleft j => sameState l1 l2 tr h mdl i j 
+         inleft j => sameState l1 l2 tr h mdl i j
       | inright h => match h i with end
         end).
 
@@ -388,12 +388,12 @@ match pIsEmpty l1 mdl with
       addIndex (pIndex l1 mdl) (fun i => MdlPredicate l2 (Tmodel l1 l2 tr (pComponents l1 mdl i))) x
         (LPTransfo (Tpred l1 l2 tr (pComponents l1 mdl x))
           (LPPred (MdlPredicate l1 (pComponents l1 mdl x)) p))
-| inright f => match f (projS1 pp) with end
+| inright f => match f (projT1 pp) with end
 end.
 
-Lemma simu_eqA: 
+Lemma simu_eqA:
   forall A1 A2 C m P sa sc tta ttc (h: A2=A1),
-  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end) 
+  simu A1 C (match h in (_=y) return mapping _ C with eq_refl => m end)
   P (match h in (_=y) return TTS y with eq_refl => sa end)
   sc (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => tta p end)
   ttc ->
@@ -401,9 +401,9 @@ Lemma simu_eqA:
 admit.
 Qed.
 
-Lemma simu_eqC: 
+Lemma simu_eqC:
   forall A C1 C2 m P sa sc tta ttc (h: C2=C1),
-  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end) 
+  simu A C1 (match h in (_=y) return mapping A _ with eq_refl => m end)
   P sa (match h in (_=y) return TTS y with eq_refl => sc end)
   tta (fun p => match h in (_=y) return LP (Predicate y _) with eq_refl => ttc p end)
    ->
@@ -411,10 +411,10 @@ Lemma simu_eqC:
 admit.
 Qed.
 
-Lemma simu_eqA1: 
+Lemma simu_eqA1:
   forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
-  simu A1 C m 
-  P 
+  simu A1 C m
+  P
   (match (sym_eq h) in (_=y) return TTS y with eq_refl => sa end) sc
   (fun p => match (sym_eq h) as e in (_=y) return LP (Predicate y (match e in (_=z) return TTS z with eq_refl => sa end)) with eq_refl => tta p end) ttc
    ->
@@ -422,32 +422,32 @@ Lemma simu_eqA1:
 admit.
 Qed.
 
-Lemma simu_eqA2: 
+Lemma simu_eqA2:
   forall A1 A2 C m P sa sc tta ttc (h: A1=A2),
   simu A1 C (match (sym_eq h) in (_=y) return mapping _ C with eq_refl => m end)
-  P 
+  P
   sa sc tta ttc
    ->
   simu A2 C m P
-  (match h in (_=y) return TTS y with eq_refl => sa end) sc 
+  (match h in (_=y) return TTS y with eq_refl => sa end) sc
   (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sa end) with eq_refl => tta p end)
  ttc.
 admit.
 Qed.
 
-Lemma simu_eqC2: 
+Lemma simu_eqC2:
   forall A C1 C2 m P sa sc tta ttc (h: C1=C2),
   simu A C1 (match (sym_eq h) in (_=y) return mapping A _ with eq_refl => m end)
-  P 
+  P
   sa sc tta ttc
    ->
   simu A C2 m P
-  sa (match h in (_=y) return TTS y with eq_refl => sc end) 
+  sa (match h in (_=y) return TTS y with eq_refl => sc end)
   tta (fun p => match h as e in (_=y) return LP (Predicate y match e in (_=y0) return TTS y0 with eq_refl => sc end) with eq_refl => ttc p end).
 admit.
 Qed.
 
-Lemma simu_eqM: 
+Lemma simu_eqM:
   forall A C m1 m2 P sa sc tta ttc (h: m1=m2),
   simu A C m1 P sa sc tta ttc
    ->
@@ -470,7 +470,7 @@ Lemma LPTransfo_addIndex:
         addIndex Ind tr1 (projT1 p0) (tr2 (projT1 p0) (projT2 p0)))
       (addIndex Ind Pred x p).
 Proof.
-  unfold addIndex; intros. 
+  unfold addIndex; intros.
   rewrite LPTransfo_trans.
   rewrite LPTransfo_trans.
   simpl.
@@ -491,7 +491,7 @@ Lemma LPTransfo_addIndex_tr:
         addIndex Ind tr1 (projT1 p0) (tr3 (projT1 p0) (tr2 (projT1 p0) (projT2 p0))))
       (addIndex Ind Pred x p).
 Proof.
-  unfold addIndex; simpl; intros. 
+  unfold addIndex; simpl; intros.
   rewrite LPTransfo_trans; simpl.
   rewrite <- LPTransfo_trans.
   f_equal.
@@ -505,19 +505,19 @@ Qed.
 Require Export Coq.Logic.FunctionalExtensionality.
 Print PLanguage.
 
-Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr): 
+Program Definition PTransfo l1 l2 (tr: Transformation l1 l2) (h: isSharedTransfo l1 l2 tr):
 Transformation (PLanguage l1) (PLanguage l2) :=
   mkTransformation (PLanguage l1) (PLanguage l2)
     (PTransfoSyntax l1 l2 tr h)
     (Pmap12 l1 l2 tr h)
     (Pmap21 l1 l2 tr h)
     (PTpred l1 l2 tr h)
-    (fun mdl => simu_equivProd 
-      (pState l1 mdl) 
-      (pState l2 (PTransfoSyntax l1 l2 tr h mdl)) 
+    (fun mdl => simu_equivProd
+      (pState l1 mdl)
+      (pState l2 (PTransfoSyntax l1 l2 tr h mdl))
       (Pmap12 l1 l2 tr h mdl)
       (Pmap21 l1 l2 tr h mdl)
-      (pIndex l1 mdl) 
+      (pIndex l1 mdl)
       (fun i => MdlPredicate l1 (pComponents l1 mdl i))
       (compSemantic l1 mdl)
       (compSemantic l2 (PTransfoSyntax l1 l2 tr h mdl))
diff --git a/test-suite/bugs/closed/4306.v b/test-suite/bugs/closed/4306.v
index 28f028ad89..80c348d207 100644
--- a/test-suite/bugs/closed/4306.v
+++ b/test-suite/bugs/closed/4306.v
@@ -1,13 +1,13 @@
 Require Import List.
 Require Import Arith.
-Require Import Recdef. 
+Require Import Recdef.
 Require Import Omega.
 
 Function foo (xys : (list nat * list nat)) {measure (fun xys => length (fst xys) + length (snd xys))} : list nat :=
   match xys with
     | (nil, _) => snd xys
     | (_, nil) => fst xys
-    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+    | (x :: xs', y :: ys') => match Nat.compare x y with
                                 | Lt => x :: foo (xs', y :: ys')
                                 | Eq => x :: foo (xs', ys')
                                 | Gt => y :: foo (x :: xs', ys')
@@ -24,7 +24,7 @@ Function bar (xys : (list nat * list nat)) {measure (fun xys => length (fst xys)
   match (xs, ys) with
     | (nil, _) => ys
     | (_, nil) => xs
-    | (x :: xs', y :: ys') => match Compare_dec.nat_compare x y with
+    | (x :: xs', y :: ys') => match Nat.compare x y with
                                 | Lt => x :: foo (xs', ys)
                                 | Eq => x :: foo (xs', ys')
                                 | Gt => y :: foo (xs, ys')
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 1307a8f26d..975b2ef7ff 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -85,8 +85,8 @@ bar : forall x : nat, x = 0
 
 Argument x is implicit and maximally inserted
 Module Coq.Init.Peano
-Notation existS2 := existT2
-Expands to: Notation Coq.Init.Specif.existS2
+Notation sym_eq := eq_sym
+Expands to: Notation Coq.Init.Logic.sym_eq
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq: Argument A is implicit and maximally inserted
diff --git a/test-suite/output/PrintInfos.v b/test-suite/output/PrintInfos.v
index a498db3e89..62aa80f8ab 100644
--- a/test-suite/output/PrintInfos.v
+++ b/test-suite/output/PrintInfos.v
@@ -26,8 +26,7 @@ About bar.
 Print bar.
 
 About Peano. (* Module *)
-Set Warnings "-deprecated".
-About existS2. (* Notation *)
+About sym_eq. (* Notation *)
 
 Arguments eq_refl {A} {x}, {A} x.
 Print eq_refl.
@@ -46,4 +45,3 @@ Goal forall n:nat, let g := newdef in n <> newdef n -> newdef n <> n -> False.
   About g.                              (* search hypothesis *)
   About h.                              (* search hypothesis *)
 Abort.
-
diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
index 06357cfc21..3c427237b4 100644
--- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
+++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v
@@ -23,7 +23,7 @@ Require Export ZArithRing.
 Tactic Notation "ElimCompare" constr(c) constr(d) := elim_compare c d.
 
 Ltac Flip :=
-  apply Zgt_lt || apply Zlt_gt || apply Zle_ge || apply Zge_le; assumption.
+  apply Z.gt_lt || apply Z.lt_gt || apply Z.le_ge || apply Z.ge_le; assumption.
 
 Ltac Falsum :=
   try intro; apply False_ind;
@@ -37,12 +37,12 @@ Ltac Falsum :=
 Ltac Step_l a :=
   match goal with
   |  |- (?X1 < ?X2)%Z => replace X1 with a; [ idtac | try ring ]
-  end. 
+  end.
 
 Ltac Step_r a :=
   match goal with
   |  |- (?X1 < ?X2)%Z => replace X2 with a; [ idtac | try ring ]
-  end. 
+  end.
 
 Ltac CaseEq formula :=
   generalize (refl_equal formula); pattern formula at -1 in |- *;
@@ -53,7 +53,7 @@ Lemma pair_1 : forall (A B : Set) (H : A * B), H = pair (fst H) (snd H).
 Proof.
  intros.
  case H.
- intros. 
+ intros.
  simpl in |- *.
  reflexivity.
 Qed.
@@ -73,10 +73,10 @@ Proof.
 Qed.
 
 
-Section projection.   
+Section projection.
  Variable A : Set.
  Variable P : A -> Prop.
- 
+
  Definition projP1 (H : sig P) := let (x, h) := H in x.
  Definition projP2 (H : sig P) :=
    let (x, h) as H return (P (projP1 H)) := H in h.
@@ -131,11 +131,11 @@ Declare Right Step neq_stepr.
 
 
 Lemma not_O_S : forall n : nat, n <> 0 -> {p : nat | n = S p}.
-Proof. 
+Proof.
  intros [| np] Hn; [ exists 0; apply False_ind; apply Hn | exists np ];
-  reflexivity. 
+  reflexivity.
 Qed.
-  
+
 
 Lemma lt_minus_neq : forall m n : nat, m < n -> n - m <> 0.
 Proof.
@@ -156,12 +156,12 @@ Proof.
 Qed.
 
 Lemma le_plus_O_l : forall p q : nat, p + q <= 0 -> p = 0.
-Proof. 
+Proof.
  intros; omega.
 Qed.
 
 Lemma le_plus_O_r : forall p q : nat, p + q <= 0 -> q = 0.
-Proof. 
+Proof.
  intros; omega.
 Qed.
 
@@ -228,8 +228,8 @@ Proof.
  assumption.
  intro.
  right.
- apply Zle_lt_trans with (m := x).
- apply Zge_le.
+ apply Z.le_lt_trans with (m := x).
+ apply Z.ge_le.
  assumption.
  assumption.
 Qed.
@@ -268,7 +268,7 @@ Proof.
  left.
  assumption.
  intro H0.
- generalize (Zge_le _ _ H0).
+ generalize (Z.ge_le _ _ H0).
  intro.
  case (Z_le_lt_eq_dec _ _ H1).
  intro.
@@ -290,25 +290,25 @@ Proof.
  left.
  assumption.
  intro H.
- generalize (Zge_le _ _ H).
+ generalize (Z.ge_le _ _ H).
  intro H0.
  case (Z_le_lt_eq_dec y x H0).
  intro H1.
  left.
  right.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  intro.
  right.
  symmetry  in |- *.
  assumption.
 Qed.
- 
+
 
 Lemma Z_dec' : forall x y : Z, {(x < y)%Z} + {(y < x)%Z} + {x = y}.
 Proof.
  intros x y.
- case (Z_eq_dec x y); intro H;
+ case (Z.eq_dec x y); intro H;
   [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
 Qed.
 
@@ -321,7 +321,7 @@ Proof.
  assumption.
  intro.
  right.
- apply Zge_le.
+ apply Z.ge_le.
  assumption.
 Qed.
 
@@ -335,7 +335,7 @@ Lemma Z_lt_lt_S_eq_dec :
 Proof.
  intros.
  generalize (Zlt_le_succ _ _ H).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  apply Z_le_lt_eq_dec.
 Qed.
 
@@ -347,7 +347,7 @@ Proof.
  case (Z_lt_le_dec a c).
  intro z.
  right.
- intro. 
+ intro.
  elim H.
  intros.
  generalize z.
@@ -356,8 +356,8 @@ Proof.
  intro.
  case (Z_lt_le_dec b d).
  intro z0.
- right. 
- intro. 
+ right.
+ intro.
  elim H.
  intros.
  generalize z0.
@@ -367,7 +367,7 @@ Proof.
  left.
  split.
  assumption.
- assumption. 
+ assumption.
 Qed.
 
 (*###########################################################################*)
@@ -386,30 +386,30 @@ Qed.
 
 Lemma Zlt_minus : forall a b : Z, (b < a)%Z -> (0 < a - b)%Z.
 Proof.
- intros a b. 
+ intros a b.
  intros.
  apply Zplus_lt_reg_l with b.
- unfold Zminus in |- *. 
+ unfold Zminus in |- *.
  rewrite (Zplus_comm a).
- rewrite (Zplus_assoc b (- b)). 
+ rewrite (Zplus_assoc b (- b)).
  rewrite Zplus_opp_r.
- simpl in |- *. 
- rewrite <- Zplus_0_r_reverse. 
+ simpl in |- *.
+ rewrite <- Zplus_0_r_reverse.
  assumption.
 Qed.
 
 
 Lemma Zle_minus : forall a b : Z, (b <= a)%Z -> (0 <= a - b)%Z.
 Proof.
- intros a b. 
+ intros a b.
  intros.
  apply Zplus_le_reg_l with b.
- unfold Zminus in |- *. 
+ unfold Zminus in |- *.
  rewrite (Zplus_comm a).
- rewrite (Zplus_assoc b (- b)). 
+ rewrite (Zplus_assoc b (- b)).
  rewrite Zplus_opp_r.
- simpl in |- *. 
- rewrite <- Zplus_0_r_reverse. 
+ simpl in |- *.
+ rewrite <- Zplus_0_r_reverse.
  assumption.
 Qed.
 
@@ -417,7 +417,7 @@ Lemma Zlt_plus_plus :
  forall m n p q : Z, (m < n)%Z -> (p < q)%Z -> (m + p < n + q)%Z.
 Proof.
  intros.
- apply Zlt_trans with (m := (n + p)%Z).
+ apply Z.lt_trans with (m := (n + p)%Z).
  rewrite Zplus_comm.
  rewrite Zplus_comm with (n := n).
  apply Zplus_lt_compat_l.
@@ -459,11 +459,11 @@ Lemma Zge_gt_plus_plus :
 Proof.
  intros.
  case (Zle_lt_or_eq n m).
- apply Zge_le.
+ apply Z.ge_le.
  assumption.
  intro.
  apply Zgt_plus_plus.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  assumption.
  intro.
@@ -521,7 +521,7 @@ Qed.
 
 
 Lemma Zle_neg_opp : forall x : Z, (x <= 0)%Z -> (0 <= - x)%Z.
-Proof. 
+Proof.
  intros.
  apply Zplus_le_reg_l with x.
  rewrite Zplus_opp_r.
@@ -530,7 +530,7 @@ Proof.
 Qed.
 
 Lemma Zle_pos_opp : forall x : Z, (0 <= x)%Z -> (- x <= 0)%Z.
-Proof. 
+Proof.
  intros.
  apply Zplus_le_reg_l with x.
  rewrite Zplus_opp_r.
@@ -542,7 +542,7 @@ Qed.
 Lemma Zge_opp : forall x y : Z, (x <= y)%Z -> (- x >= - y)%Z.
 Proof.
  intros.
- apply Zle_ge.
+ apply Z.le_ge.
  apply Zplus_le_reg_l with (p := (x + y)%Z).
  ring_simplify (x + y + - y)%Z (x + y + - x)%Z.
  assumption.
@@ -584,8 +584,8 @@ Proof.
  ring_simplify (- a * x + a * x)%Z.
  replace (- a * x + a * y)%Z with ((y - x) * a)%Z.
  apply Zmult_gt_0_le_0_compat.
- apply Zlt_gt.
- assumption. 
+ apply Z.lt_gt.
+ assumption.
  unfold Zminus in |- *.
  apply Zle_left.
  assumption.
@@ -621,7 +621,7 @@ Proof.
  rewrite H0.
  reflexivity.
 Qed.
- 
+
 Lemma Zsimpl_mult_l :
  forall n m p : Z, n <> 0%Z -> (n * m)%Z = (n * p)%Z -> m = p.
 Proof.
@@ -642,14 +642,14 @@ Lemma Zlt_reg_mult_l :
 Proof.
  intros.
  case (Zcompare_Gt_spec x 0).
- unfold Zgt in H.
+ unfold Z.gt in H.
  assumption.
  intros.
- cut (x = Zpos x0). 
+ cut (x = Zpos x0).
  intro.
  rewrite H2.
- unfold Zlt in H0.
- unfold Zlt in |- *.
+ unfold Z.lt in H0.
+ unfold Z.lt in |- *.
  cut ((Zpos x0 * y ?= Zpos x0 * z)%Z = (y ?= z)%Z).
  intro.
  exact (trans_eq H3 H0).
@@ -672,10 +672,10 @@ Proof.
  intro.
  cut ((y ?= x)%Z = (- x ?= - y)%Z).
  intro.
- exact (trans_eq H0 H1). 
+ exact (trans_eq H0 H1).
  exact (Zcompare_opp y x).
  apply sym_eq.
- exact (Zlt_gt x y H).
+ exact (Z.lt_gt x y H).
 Qed.
 
 
@@ -698,22 +698,22 @@ Proof.
  intro.
  rewrite H6 in H4.
  assumption.
- exact (Zopp_involutive (x * z)).
- exact (Zopp_involutive (x * y)).
+ exact (Z.opp_involutive (x * z)).
+ exact (Z.opp_involutive (x * y)).
  cut ((- (- x * y))%Z = (- - (x * y))%Z).
  intro.
  rewrite H4 in H3.
- cut ((- (- x * z))%Z = (- - (x * z))%Z). 
+ cut ((- (- x * z))%Z = (- - (x * z))%Z).
  intro.
  rewrite H5 in H3.
  assumption.
  cut ((- x * z)%Z = (- (x * z))%Z).
  intro.
- exact (f_equal Zopp H5).
+ exact (f_equal Z.opp H5).
  exact (Zopp_mult_distr_l_reverse x z).
  cut ((- x * y)%Z = (- (x * y))%Z).
  intro.
- exact (f_equal Zopp H4).
+ exact (f_equal Z.opp H4).
  exact (Zopp_mult_distr_l_reverse x y).
  exact (Zlt_opp (- x * y) (- x * z) H2).
  exact (Zlt_reg_mult_l (- x) y z H1 H0).
@@ -735,14 +735,14 @@ Proof.
  assumption.
  exact (sym_eq H2).
  exact (Zorder.Zlt_not_eq y x H0).
- exact (Zgt_lt x y H).
+ exact (Z.gt_lt x y H).
 Qed.
 
 Lemma Zmult_resp_nonzero :
  forall x y : Z, x <> 0%Z -> y <> 0%Z -> (x * y)%Z <> 0%Z.
 Proof.
  intros x y Hx Hy Hxy.
- apply Hx. 
+ apply Hx.
  apply Zmult_integral_l with y; assumption.
 Qed.
 
@@ -769,12 +769,12 @@ Qed.
 
 Lemma not_Zle_lt : forall x y : Z, ~ (y <= x)%Z -> (x < y)%Z.
 Proof.
- intros; apply Zgt_lt; apply Znot_le_gt; assumption.
+ intros; apply Z.gt_lt; apply Znot_le_gt; assumption.
 Qed.
 
 Lemma not_Zlt : forall x y : Z, ~ (y < x)%Z -> (x <= y)%Z.
 Proof.
- intros x y H1 H2; apply H1; apply Zgt_lt; assumption.
+ intros x y H1 H2; apply H1; apply Z.gt_lt; assumption.
 Qed.
 
 
@@ -813,7 +813,7 @@ Proof.
  cut (x > 0)%Z.
  intro.
  exact (Zlt_reg_mult_l x y z H4 H2).
- exact (Zlt_gt 0 x H3).
+ exact (Z.lt_gt 0 x H3).
  intro.
  apply False_ind.
  cut (x * z < x * y)%Z.
@@ -849,7 +849,7 @@ Proof.
  cut (x > 0)%Z.
  intro.
  exact (Zlt_reg_mult_l x z y H4 H2).
- exact (Zlt_gt 0 x H3).
+ exact (Z.lt_gt 0 x H3).
 Qed.
 
 Lemma Zlt_mult_mult :
@@ -857,9 +857,9 @@ Lemma Zlt_mult_mult :
  (0 < a)%Z -> (0 < d)%Z -> (a < b)%Z -> (c < d)%Z -> (a * c < b * d)%Z.
 Proof.
  intros.
- apply Zlt_trans with (a * d)%Z.
+ apply Z.lt_trans with (a * d)%Z.
  apply Zlt_reg_mult_l.
- Flip. 
+ Flip.
  assumption.
  rewrite Zmult_comm.
  rewrite Zmult_comm with b d.
@@ -881,11 +881,11 @@ Proof.
  apply Zgt_not_eq.
  assumption.
  trivial.
- 
+
  intro.
  case (not_Zeq x y H1).
  trivial.
- 
+
  intro.
  apply False_ind.
  cut (a * y > a * x)%Z.
@@ -913,14 +913,14 @@ Proof.
  rewrite Zmult_opp_opp.
  rewrite Zmult_opp_opp.
  assumption.
- apply Zopp_involutive.
- apply Zopp_involutive.
- apply Zgt_lt.
+ apply Z.opp_involutive.
+ apply Z.opp_involutive.
+ apply Z.gt_lt.
  apply Zlt_opp.
- apply Zgt_lt.
+ apply Z.gt_lt.
  assumption.
  simpl in |- *.
- rewrite Zopp_involutive.
+ rewrite Z.opp_involutive.
  assumption.
 Qed.
 
@@ -944,7 +944,7 @@ Proof.
  constructor.
  replace (-1 * y)%Z with (- y)%Z.
  replace (-1 * x)%Z with (- x)%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  ring.
  ring.
@@ -959,13 +959,13 @@ Proof.
  trivial.
  intro.
  apply False_ind.
- apply (Zlt_irrefl (a * x)).
- apply Zle_lt_trans with (m := (a * y)%Z).
+ apply (Z.lt_irrefl (a * x)).
+ apply Z.le_lt_trans with (m := (a * y)%Z).
  assumption.
- apply Zgt_lt.
+ apply Z.gt_lt.
  apply Zlt_conv_mult_l.
  assumption.
- apply Zgt_lt.
+ apply Z.gt_lt.
  assumption.
 Qed.
 
@@ -973,17 +973,17 @@ Lemma Zlt_mult_cancel_l :
  forall x y z : Z, (0 < x)%Z -> (x * y < x * z)%Z -> (y < z)%Z.
 Proof.
  intros.
- apply Zgt_lt.
+ apply Z.gt_lt.
  apply Zgt_mult_reg_absorb_l with x.
- apply Zlt_gt.
- assumption. 
- apply Zlt_gt.
+ apply Z.lt_gt.
+ assumption.
+ apply Z.lt_gt.
  assumption.
 Qed.
- 
+
 
 Lemma Zmin_cancel_Zle : forall x y : Z, (- x <= - y)%Z -> (y <= x)%Z.
-Proof. 
+Proof.
  intros.
  apply Zmult_cancel_Zle with (a := (-1)%Z).
  constructor.
@@ -1004,18 +1004,18 @@ Proof.
  trivial.
  intro.
  apply False_ind.
- apply (Zlt_irrefl (a * y)).
- apply Zle_lt_trans with (m := (a * x)%Z).
+ apply (Z.lt_irrefl (a * y)).
+ apply Z.le_lt_trans with (m := (a * x)%Z).
  assumption.
  apply Zlt_reg_mult_l.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
- apply Zgt_lt.
+ apply Z.gt_lt.
  assumption.
 Qed.
 
 Lemma Zopp_Zle : forall x y : Z, (y <= x)%Z -> (- x <= - y)%Z.
-Proof. 
+Proof.
  intros.
  apply Zmult_cancel_Zle with (a := (-1)%Z).
  constructor.
@@ -1026,7 +1026,7 @@ Proof.
  clear x H; ring.
 Qed.
 
- 
+
 Lemma Zle_lt_eq_S : forall x y : Z, (x <= y)%Z -> (y < x + 1)%Z -> y = x.
 Proof.
  intros.
@@ -1035,8 +1035,8 @@ Proof.
  apply False_ind.
  generalize (Zlt_le_succ x y H1).
  intro.
- apply (Zlt_not_le y (x + 1) H0).  
- replace (x + 1)%Z with (Zsucc x).
+ apply (Zlt_not_le y (x + 1) H0).
+ replace (x + 1)%Z with (Z.succ x).
  assumption.
  reflexivity.
  intro H1.
@@ -1053,8 +1053,8 @@ Proof.
  apply False_ind.
  generalize (Zlt_le_succ x y H).
  intro.
- apply (Zlt_not_le y (x + 1) H1).  
- replace (x + 1)%Z with (Zsucc x).
+ apply (Zlt_not_le y (x + 1) H1).
+ replace (x + 1)%Z with (Z.succ x).
  assumption.
  reflexivity.
  trivial.
@@ -1067,9 +1067,9 @@ Proof.
  intros.
  case (Z_zerop c).
  intro.
- rewrite e.  
+ rewrite e.
  left.
- apply sym_not_eq. 
+ apply sym_not_eq.
  intro.
  apply H; repeat split; assumption.
  intro; right; assumption.
@@ -1085,21 +1085,21 @@ Proof.
                   [ apply False_ind; apply H; repeat split | right; right ]
                | right; left ]
             | left ]; assumption.
-Qed. 
+Qed.
 
 Lemma mediant_1 :
  forall m n m' n' : Z, (m' * n < m * n')%Z -> ((m + m') * n < m * (n + n'))%Z.
 Proof.
- intros. 
- rewrite Zmult_plus_distr_r. 
+ intros.
+ rewrite Zmult_plus_distr_r.
  rewrite Zmult_plus_distr_l.
  apply Zplus_lt_compat_l.
  assumption.
 Qed.
- 
+
 Lemma mediant_2 :
  forall m n m' n' : Z,
- (m' * n < m * n')%Z -> (m' * (n + n') < (m + m') * n')%Z. 
+ (m' * n < m * n')%Z -> (m' * (n + n') < (m + m') * n')%Z.
 Proof.
  intros.
  rewrite Zmult_plus_distr_l.
@@ -1121,7 +1121,7 @@ Proof.
  assumption.
  assumption.
  ring.
-Qed. 
+Qed.
 
 Lemma fraction_lt_trans :
  forall a b c d e f : Z,
@@ -1130,21 +1130,21 @@ Lemma fraction_lt_trans :
  (0 < f)%Z -> (a * d < c * b)%Z -> (c * f < e * d)%Z -> (a * f < e * b)%Z.
 Proof.
  intros.
- apply Zgt_lt.
+ apply Z.gt_lt.
  apply Zgt_mult_reg_absorb_l with d.
  Flip.
  apply Zgt_trans with (c * b * f)%Z.
  replace (d * (e * b))%Z with (b * (e * d))%Z.
  replace (c * b * f)%Z with (b * (c * f))%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  apply Zlt_reg_mult_l.
  Flip.
  assumption.
  ring.
  ring.
- replace (c * b * f)%Z with (f * (c * b))%Z.  
+ replace (c * b * f)%Z with (f * (c * b))%Z.
  replace (d * (a * f))%Z with (f * (a * d))%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  apply Zlt_reg_mult_l.
  Flip.
  assumption.
@@ -1157,7 +1157,7 @@ Lemma square_pos : forall a : Z, a <> 0%Z -> (0 < a * a)%Z.
 Proof.
  intros [| p| p]; intros; [ Falsum | constructor | constructor ].
 Qed.
- 
+
 Hint Resolve square_pos: zarith.
 
 (*###########################################################################*)
@@ -1182,19 +1182,19 @@ Proof.
  intros.
  unfold Z_of_nat in |- *.
  rewrite H0.
- 
+
  apply f_equal with (A := positive) (B := Z) (f := Zpos).
  cut (P_of_succ_nat (nat_of_P p) = P_of_succ_nat (S x)).
  intro.
  rewrite P_of_succ_nat_o_nat_of_P_eq_succ in H1.
- cut (Ppred (Psucc p) = Ppred (P_of_succ_nat (S x))).
+ cut (Pos.pred (Pos.succ p) = Pos.pred (P_of_succ_nat (S x))).
  intro.
- rewrite Ppred_succ in H2.
+ rewrite Pos.pred_succ in H2.
  simpl in H2.
- rewrite Ppred_succ in H2.
+ rewrite Pos.pred_succ in H2.
  apply sym_eq.
  assumption.
- apply f_equal with (A := positive) (B := positive) (f := Ppred).
+ apply f_equal with (A := positive) (B := positive) (f := Pos.pred).
  assumption.
  apply f_equal with (f := P_of_succ_nat).
  assumption.
@@ -1222,7 +1222,7 @@ Lemma NEG_neq_ZERO : forall p : positive, Zneg p <> 0%Z.
 Proof.
  intros.
  apply Zorder.Zlt_not_eq.
- unfold Zlt in |- *.
+ unfold Z.lt in |- *.
  constructor.
 Qed.
 
@@ -1237,7 +1237,7 @@ Qed.
 Lemma nat_nat_pos : forall m n : nat, ((m + 1) * (n + 1) > 0)%Z. (*QF*)
 Proof.
  intros.
- apply Zlt_gt.
+ apply Z.lt_gt.
  cut (Z_of_nat m + 1 > 0)%Z.
  intro.
  cut (0 < Z_of_nat n + 1)%Z.
@@ -1246,24 +1246,24 @@ Proof.
  rewrite Zmult_0_r.
  intro.
  assumption.
- 
+
  apply Zlt_reg_mult_l.
  assumption.
  assumption.
- change (0 < Zsucc (Z_of_nat n))%Z in |- *.
+ change (0 < Z.succ (Z_of_nat n))%Z in |- *.
  apply Zle_lt_succ.
  change (Z_of_nat 0 <= Z_of_nat n)%Z in |- *.
  apply Znat.inj_le.
  apply le_O_n.
- apply Zlt_gt.
- change (0 < Zsucc (Z_of_nat m))%Z in |- *.
+ apply Z.lt_gt.
+ change (0 < Z.succ (Z_of_nat m))%Z in |- *.
  apply Zle_lt_succ.
  change (Z_of_nat 0 <= Z_of_nat m)%Z in |- *.
  apply Znat.inj_le.
  apply le_O_n.
 Qed.
- 
- 
+
+
 Theorem S_predn : forall m : nat, m <> 0 -> S (pred m) = m. (*QF*)
 Proof.
  intros.
@@ -1271,8 +1271,8 @@ Proof.
  intro.
  case s.
  intros.
- rewrite <- e. 
- rewrite <- pred_Sn with (n := x). 
+ rewrite <- e.
+ rewrite <- pred_Sn with (n := x).
  trivial.
  intro.
  apply False_ind.
@@ -1281,7 +1281,7 @@ Proof.
  assumption.
 Qed.
 
-Lemma absolu_1 : forall x : Z, Zabs_nat x = 0 -> x = 0%Z. (*QF*)
+Lemma absolu_1 : forall x : Z, Z.abs_nat x = 0 -> x = 0%Z. (*QF*)
 Proof.
  intros.
  case (dec_eq x 0).
@@ -1302,15 +1302,15 @@ Proof.
  apply proj1 with (B := x = 0%Z -> (x ?= 0)%Z = Datatypes.Eq).
  change ((x ?= 0)%Z = Datatypes.Eq <-> x = 0%Z) in |- *.
  apply Zcompare_Eq_iff_eq.
- 
+
  (***)
  intro.
- cut (exists h : nat, Zabs_nat x = S h).
+ cut (exists h : nat, Z.abs_nat x = S h).
  intro.
  case H3.
  rewrite H.
  exact O_S.
- 
+
  change (x < 0)%Z in H2.
  cut (0 > x)%Z.
  intro.
@@ -1324,7 +1324,7 @@ Proof.
  case H6.
  intros.
  rewrite H7.
- unfold Zabs_nat in |- *.
+ unfold Z.abs_nat in |- *.
  generalize x1.
  exact ZL4.
  cut (x = (- Zpos x0)%Z).
@@ -1335,21 +1335,21 @@ Proof.
  cut ((- - x)%Z = x).
  intro.
  rewrite <- H6.
- exact (f_equal Zopp H5). 
- apply Zopp_involutive.
+ exact (f_equal Z.opp H5).
+ apply Z.opp_involutive.
  apply Zcompare_Gt_spec.
  assumption.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
- 
+
  (***)
  intro.
- cut (exists h : nat, Zabs_nat x = S h).
+ cut (exists h : nat, Z.abs_nat x = S h).
  intro.
  case H3.
  rewrite H.
  exact O_S.
- 
+
  cut (exists p : positive, (x + - (0))%Z = Zpos p).
  simpl in |- *.
  rewrite Zplus_0_r.
@@ -1357,12 +1357,12 @@ Proof.
  case H3.
  intros.
  rewrite H4.
- unfold Zabs_nat in |- *.
+ unfold Z.abs_nat in |- *.
  generalize x0.
  exact ZL4.
  apply Zcompare_Gt_spec.
  assumption.
- 
+
  (***)
  cut ((x < 0)%Z \/ (0 < x)%Z).
  intro.
@@ -1373,14 +1373,14 @@ Proof.
  assumption.
  intro.
  right.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  assumption.
  apply not_Zeq.
  assumption.
 Qed.
 
-Lemma absolu_2 : forall x : Z, x <> 0%Z -> Zabs_nat x <> 0. (*QF*)
+Lemma absolu_2 : forall x : Z, x <> 0%Z -> Z.abs_nat x <> 0. (*QF*)
 Proof.
  intros.
  intro.
@@ -1392,7 +1392,7 @@ Qed.
 
 
 
-Lemma absolu_inject_nat : forall n : nat, Zabs_nat (Z_of_nat n) = n.
+Lemma absolu_inject_nat : forall n : nat, Z.abs_nat (Z_of_nat n) = n.
 Proof.
  simple induction n; simpl in |- *.
  reflexivity.
@@ -1404,7 +1404,7 @@ Qed.
 Lemma eq_inj : forall m n : nat, m = n :>Z -> m = n.
 Proof.
  intros.
- generalize (f_equal Zabs_nat H). 
+ generalize (f_equal Z.abs_nat H).
  intro.
  rewrite (absolu_inject_nat m) in H0.
  rewrite (absolu_inject_nat n) in H0.
@@ -1438,7 +1438,7 @@ Qed.
 
 Lemma le_absolu :
  forall x y : Z,
- (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Zabs_nat x <= Zabs_nat y.
+ (0 <= x)%Z -> (0 <= y)%Z -> (x <= y)%Z -> Z.abs_nat x <= Z.abs_nat y.
 Proof.
  intros [| x| x] [| y| y] Hx Hy Hxy;
   apply le_O_n ||
@@ -1451,7 +1451,7 @@ Proof.
       | id1:(Zpos _ <= Zneg _)%Z |- _ =>
           apply False_ind; apply id1; constructor
       end).
- simpl in |- *. 
+ simpl in |- *.
  apply le_inj.
  do 2 rewrite ZL9.
  assumption.
@@ -1459,7 +1459,7 @@ Qed.
 
 Lemma lt_absolu :
  forall x y : Z,
- (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Zabs_nat x < Zabs_nat y.
+ (0 <= x)%Z -> (0 <= y)%Z -> (x < y)%Z -> Z.abs_nat x < Z.abs_nat y.
 Proof.
  intros [| x| x] [| y| y] Hx Hy Hxy; inversion Hxy;
   try
@@ -1470,13 +1470,13 @@ Proof.
        apply False_ind; apply id1; constructor
    | id1:(Zpos _ <= Zneg _)%Z |- _ =>
        apply False_ind; apply id1; constructor
-   end; simpl in |- *; apply lt_inj; repeat rewrite ZL9; 
+   end; simpl in |- *; apply lt_inj; repeat rewrite ZL9;
   assumption.
 Qed.
 
 Lemma absolu_plus :
  forall x y : Z,
- (0 <= x)%Z -> (0 <= y)%Z -> Zabs_nat (x + y) = Zabs_nat x + Zabs_nat y.
+ (0 <= x)%Z -> (0 <= y)%Z -> Z.abs_nat (x + y) = Z.abs_nat x + Z.abs_nat y.
 Proof.
  intros [| x| x] [| y| y] Hx Hy; trivial;
   try
@@ -1489,23 +1489,23 @@ Proof.
        apply False_ind; apply id1; constructor
    end.
  rewrite <- BinInt.Zpos_plus_distr.
- unfold Zabs_nat in |- *.
+ unfold Z.abs_nat in |- *.
  apply nat_of_P_plus_morphism.
 Qed.
 
 Lemma pred_absolu :
- forall x : Z, (0 < x)%Z -> pred (Zabs_nat x) = Zabs_nat (x - 1).
+ forall x : Z, (0 < x)%Z -> pred (Z.abs_nat x) = Z.abs_nat (x - 1).
 Proof.
  intros x Hx.
  generalize (Z_lt_lt_S_eq_dec 0 x Hx); simpl in |- *; intros [H1| H1];
-  [ replace (Zabs_nat x) with (Zabs_nat (x - 1 + 1));
+  [ replace (Z.abs_nat x) with (Z.abs_nat (x - 1 + 1));
      [ idtac | apply f_equal with Z; auto with zarith ];
      rewrite absolu_plus;
-     [ unfold Zabs_nat at 2, nat_of_P, Piter_op in |- *; omega
+     [ unfold Z.abs_nat at 2, nat_of_P, Pos.iter_op in |- *; omega
      | auto with zarith
      | intro; discriminate ]
   | rewrite <- H1; reflexivity ].
-Qed. 
+Qed.
 
 Definition pred_nat : forall (x : Z) (Hx : (0 < x)%Z), nat.
 intros [| px| px] Hx; try abstract (discriminate Hx).
@@ -1535,7 +1535,7 @@ Proof.
 Qed.
 
 Lemma absolu_pred_nat :
- forall (m : Z) (Hm : (0 < m)%Z), S (pred_nat m Hm) = Zabs_nat m.
+ forall (m : Z) (Hm : (0 < m)%Z), S (pred_nat m Hm) = Z.abs_nat m.
 Proof.
  intros [| px| px] Hx; try discriminate Hx.
  unfold pred_nat in |- *.
@@ -1545,7 +1545,7 @@ Proof.
 Qed.
 
 Lemma pred_nat_absolu :
- forall (m : Z) (Hm : (0 < m)%Z), pred_nat m Hm = Zabs_nat (m - 1).
+ forall (m : Z) (Hm : (0 < m)%Z), pred_nat m Hm = Z.abs_nat (m - 1).
 Proof.
  intros [| px| px] Hx; try discriminate Hx.
  unfold pred_nat in |- *.
@@ -1557,15 +1557,15 @@ Lemma minus_pred_nat :
  S (pred_nat n Hn) - S (pred_nat m Hm) = S (pred_nat (n - m) Hnm).
 Proof.
  intros.
- simpl in |- *.  
+ simpl in |- *.
  destruct n; try discriminate Hn.
  destruct m; try discriminate Hm.
  unfold pred_nat at 1 2 in |- *.
  rewrite minus_pred; try apply lt_O_nat_of_P.
  apply eq_inj.
- rewrite <- pred_nat_unfolded. 
+ rewrite <- pred_nat_unfolded.
  rewrite Znat.inj_minus1.
- repeat rewrite ZL9. 
+ repeat rewrite ZL9.
  reflexivity.
  apply le_inj.
  apply Zlt_le_weak.
@@ -1581,13 +1581,13 @@ Qed.
 
 
 Lemma Zsgn_1 :
- forall x : Z, {Zsgn x = 0%Z} + {Zsgn x = 1%Z} + {Zsgn x = (-1)%Z}. (*QF*)
+ forall x : Z, {Z.sgn x = 0%Z} + {Z.sgn x = 1%Z} + {Z.sgn x = (-1)%Z}. (*QF*)
 Proof.
  intros.
  case x.
  left.
  left.
- unfold Zsgn in |- *.
+ unfold Z.sgn in |- *.
  reflexivity.
  intro.
  simpl in |- *.
@@ -1601,13 +1601,13 @@ Proof.
 Qed.
 
 
-Lemma Zsgn_2 : forall x : Z, Zsgn x = 0%Z -> x = 0%Z.   (*QF*)
+Lemma Zsgn_2 : forall x : Z, Z.sgn x = 0%Z -> x = 0%Z.   (*QF*)
 Proof.
  intros [| p1| p1]; simpl in |- *; intro H; constructor || discriminate H.
 Qed.
 
 
-Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Zsgn x <> 0%Z.   (*QF*)
+Lemma Zsgn_3 : forall x : Z, x <> 0%Z -> Z.sgn x <> 0%Z.   (*QF*)
 Proof.
  intro.
  case x.
@@ -1626,21 +1626,21 @@ Qed.
 
 
 
-Theorem Zsgn_4 : forall a : Z, a = (Zsgn a * Zabs_nat a)%Z.  (*QF*)
+Theorem Zsgn_4 : forall a : Z, a = (Z.sgn a * Z.abs_nat a)%Z.  (*QF*)
 Proof.
  intro.
  case a.
  simpl in |- *.
  reflexivity.
  intro.
- unfold Zsgn in |- *.
- unfold Zabs_nat in |- *.
+ unfold Z.sgn in |- *.
+ unfold Z.abs_nat in |- *.
  rewrite Zmult_1_l.
  symmetry  in |- *.
  apply ZL9.
  intros.
- unfold Zsgn in |- *.
- unfold Zabs_nat in |- *.
+ unfold Z.sgn in |- *.
+ unfold Z.abs_nat in |- *.
  rewrite ZL9.
  constructor.
 Qed.
@@ -1650,7 +1650,7 @@ Theorem Zsgn_5 :
  forall a b x y : Z,
  x <> 0%Z ->
  y <> 0%Z ->
- (Zsgn a * x)%Z = (Zsgn b * y)%Z -> (Zsgn a * y)%Z = (Zsgn b * x)%Z.  (*QF*)
+ (Z.sgn a * x)%Z = (Z.sgn b * y)%Z -> (Z.sgn a * y)%Z = (Z.sgn b * x)%Z.  (*QF*)
 Proof.
  intros a b x y H H0.
  case a.
@@ -1660,7 +1660,7 @@ Proof.
  trivial.
 
  intro.
- unfold Zsgn in |- *.
+ unfold Z.sgn in |- *.
  intro.
  rewrite Zmult_1_l in H1.
  simpl in H1.
@@ -1669,11 +1669,11 @@ Proof.
  symmetry  in |- *.
  assumption.
  intro.
- unfold Zsgn in |- *.
+ unfold Z.sgn in |- *.
  intro.
  apply False_ind.
  apply H0.
- apply Zopp_inj.
+ apply Z.opp_inj.
  simpl in |- *.
  transitivity (-1 * y)%Z.
  constructor.
@@ -1683,13 +1683,13 @@ Proof.
  simpl in |- *.
  reflexivity.
  intro.
- unfold Zsgn at 1 in |- *.
- unfold Zsgn at 2 in |- *.
+ unfold Z.sgn at 1 in |- *.
+ unfold Z.sgn at 2 in |- *.
  intro.
  transitivity y.
  rewrite Zmult_1_l.
  reflexivity.
- transitivity (Zsgn b * (Zsgn b * y))%Z.
+ transitivity (Z.sgn b * (Z.sgn b * y))%Z.
  case (Zsgn_1 b).
  intro.
  case s.
@@ -1712,20 +1712,20 @@ Proof.
  rewrite H1.
  reflexivity.
  intro.
- unfold Zsgn at 1 in |- *.
- unfold Zsgn at 2 in |- *.
+ unfold Z.sgn at 1 in |- *.
+ unfold Z.sgn at 2 in |- *.
  intro.
- transitivity (Zsgn b * (-1 * (Zsgn b * y)))%Z.
+ transitivity (Z.sgn b * (-1 * (Z.sgn b * y)))%Z.
  case (Zsgn_1 b).
  intros.
  case s.
  intro.
  apply False_ind.
  apply H.
- apply Zopp_inj.
+ apply Z.opp_inj.
  transitivity (-1 * x)%Z.
  ring.
- unfold Zopp in |- *.
+ unfold Z.opp in |- *.
  rewrite e in H1.
  transitivity (0 * y)%Z.
  assumption.
@@ -1741,7 +1741,7 @@ Proof.
  ring.
 Qed.
 
-Lemma Zsgn_6 : forall x : Z, x = 0%Z -> Zsgn x = 0%Z.
+Lemma Zsgn_6 : forall x : Z, x = 0%Z -> Z.sgn x = 0%Z.
 Proof.
  intros.
  rewrite H.
@@ -1750,44 +1750,44 @@ Proof.
 Qed.
 
 
-Lemma Zsgn_7 : forall x : Z, (x > 0)%Z -> Zsgn x = 1%Z.
+Lemma Zsgn_7 : forall x : Z, (x > 0)%Z -> Z.sgn x = 1%Z.
 Proof.
  intro.
  case x.
  intro.
  apply False_ind.
- apply (Zlt_irrefl 0).
+ apply (Z.lt_irrefl 0).
  Flip.
  intros.
  simpl in |- *.
  reflexivity.
  intros.
  apply False_ind.
- apply (Zlt_irrefl (Zneg p)).
- apply Zlt_trans with 0%Z.
+ apply (Z.lt_irrefl (Zneg p)).
+ apply Z.lt_trans with 0%Z.
  constructor.
  Flip.
 Qed.
 
 
-Lemma Zsgn_7' : forall x : Z, (0 < x)%Z -> Zsgn x = 1%Z.
+Lemma Zsgn_7' : forall x : Z, (0 < x)%Z -> Z.sgn x = 1%Z.
 Proof.
  intros; apply Zsgn_7; Flip.
 Qed.
 
 
-Lemma Zsgn_8 : forall x : Z, (x < 0)%Z -> Zsgn x = (-1)%Z.
+Lemma Zsgn_8 : forall x : Z, (x < 0)%Z -> Z.sgn x = (-1)%Z.
 Proof.
  intro.
  case x.
  intro.
  apply False_ind.
- apply (Zlt_irrefl 0).
+ apply (Z.lt_irrefl 0).
  assumption.
  intros.
  apply False_ind.
- apply (Zlt_irrefl 0).
- apply Zlt_trans with (Zpos p).
+ apply (Z.lt_irrefl 0).
+ apply Z.lt_trans with (Zpos p).
  constructor.
  assumption.
  intros.
@@ -1795,7 +1795,7 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zsgn_9 : forall x : Z, Zsgn x = 1%Z -> (0 < x)%Z.
+Lemma Zsgn_9 : forall x : Z, Z.sgn x = 1%Z -> (0 < x)%Z.
 Proof.
  intro.
  case x.
@@ -1809,8 +1809,8 @@ Proof.
  apply False_ind.
  discriminate.
 Qed.
- 
-Lemma Zsgn_10 : forall x : Z, Zsgn x = (-1)%Z -> (x < 0)%Z.
+
+Lemma Zsgn_10 : forall x : Z, Z.sgn x = (-1)%Z -> (x < 0)%Z.
 Proof.
  intro.
  case x.
@@ -1822,9 +1822,9 @@ Proof.
  discriminate.
  intros.
  constructor.
-Qed. 
+Qed.
 
-Lemma Zsgn_11 : forall x : Z, (Zsgn x < 0)%Z -> (x < 0)%Z.
+Lemma Zsgn_11 : forall x : Z, (Z.sgn x < 0)%Z -> (x < 0)%Z.
 Proof.
  intros.
  apply Zsgn_10.
@@ -1833,7 +1833,7 @@ Proof.
  apply False_ind.
  case s.
  intro.
- generalize (Zorder.Zlt_not_eq _ _ H). 
+ generalize (Zorder.Zlt_not_eq _ _ H).
  intro.
  apply (H0 e).
  intro.
@@ -1842,9 +1842,9 @@ Proof.
  intro.
  discriminate.
  trivial.
-Qed. 
+Qed.
 
-Lemma Zsgn_12 : forall x : Z, (0 < Zsgn x)%Z -> (0 < x)%Z.
+Lemma Zsgn_12 : forall x : Z, (0 < Z.sgn x)%Z -> (0 < x)%Z.
 Proof.
  intros.
  apply Zsgn_9.
@@ -1852,7 +1852,7 @@ Proof.
  intro.
  case s.
  intro.
- generalize (Zorder.Zlt_not_eq _ _ H). 
+ generalize (Zorder.Zlt_not_eq _ _ H).
  intro.
  generalize (sym_eq e).
  intro.
@@ -1865,78 +1865,78 @@ Proof.
  intro.
  apply False_ind.
  discriminate.
-Qed.   
+Qed.
 
-Lemma Zsgn_13 : forall x : Z, (0 <= Zsgn x)%Z -> (0 <= x)%Z.
+Lemma Zsgn_13 : forall x : Z, (0 <= Z.sgn x)%Z -> (0 <= x)%Z.
 Proof.
- intros. 
- case (Z_le_lt_eq_dec 0 (Zsgn x) H).
+ intros.
+ case (Z_le_lt_eq_dec 0 (Z.sgn x) H).
  intro.
  apply Zlt_le_weak.
  apply Zsgn_12.
- assumption. 
+ assumption.
  intro.
- assert (x = 0%Z). 
+ assert (x = 0%Z).
  apply Zsgn_2.
  symmetry  in |- *.
  assumption.
  rewrite H0.
- apply Zle_refl.
+ apply Z.le_refl.
 Qed.
 
-Lemma Zsgn_14 : forall x : Z, (Zsgn x <= 0)%Z -> (x <= 0)%Z.
+Lemma Zsgn_14 : forall x : Z, (Z.sgn x <= 0)%Z -> (x <= 0)%Z.
 Proof.
- intros. 
- case (Z_le_lt_eq_dec (Zsgn x) 0 H).
+ intros.
+ case (Z_le_lt_eq_dec (Z.sgn x) 0 H).
  intro.
  apply Zlt_le_weak.
  apply Zsgn_11.
- assumption. 
+ assumption.
  intro.
- assert (x = 0%Z). 
+ assert (x = 0%Z).
  apply Zsgn_2.
  assumption.
  rewrite H0.
- apply Zle_refl.
+ apply Z.le_refl.
 Qed.
 
-Lemma Zsgn_15 : forall x y : Z, Zsgn (x * y) = (Zsgn x * Zsgn y)%Z.
+Lemma Zsgn_15 : forall x y : Z, Z.sgn (x * y) = (Z.sgn x * Z.sgn y)%Z.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; constructor.
 Qed.
 
 Lemma Zsgn_16 :
  forall x y : Z,
- Zsgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}.
+ Z.sgn (x * y) = 1%Z -> {(0 < x)%Z /\ (0 < y)%Z} + {(x < 0)%Z /\ (y < 0)%Z}.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right ]; repeat split.
-Qed. 
+Qed.
 
 Lemma Zsgn_17 :
  forall x y : Z,
- Zsgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}.
+ Z.sgn (x * y) = (-1)%Z -> {(0 < x)%Z /\ (y < 0)%Z} + {(x < 0)%Z /\ (0 < y)%Z}.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right ]; repeat split.
-Qed. 
+Qed.
 
-Lemma Zsgn_18 : forall x y : Z, Zsgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}.
+Lemma Zsgn_18 : forall x y : Z, Z.sgn (x * y) = 0%Z -> {x = 0%Z} + {y = 0%Z}.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   try discriminate H; [ left | right | right ]; constructor.
-Qed. 
+Qed.
 
 
 
-Lemma Zsgn_19 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 < x + y)%Z.
+Lemma Zsgn_19 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 < x + y)%Z.
 Proof.
  Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
   discriminate H || (constructor || apply Zsgn_12; assumption).
 Qed.
 
-Lemma Zsgn_20 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x + y < 0)%Z.
+Lemma Zsgn_20 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x + y < 0)%Z.
 Proof.
  Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intro H;
@@ -1944,43 +1944,43 @@ Proof.
 Qed.
 
 
-Lemma Zsgn_21 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= x)%Z.
+Lemma Zsgn_21 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 <= x)%Z.
 Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_22 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (x <= 0)%Z.
+Lemma Zsgn_22 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (x <= 0)%Z.
 Proof.
  Proof.
  intros [|p1|p1]; [intros y|intros [|p2|p2] ..]; simpl in |- *; intros H H0;
   discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_23 : forall x y : Z, (0 < Zsgn x + Zsgn y)%Z -> (0 <= y)%Z.
+Lemma Zsgn_23 : forall x y : Z, (0 < Z.sgn x + Z.sgn y)%Z -> (0 <= y)%Z.
 Proof.
  intros [|p1|p1] [|p2|p2]; simpl in |- *;
   intros H H0; discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_24 : forall x y : Z, (Zsgn x + Zsgn y < 0)%Z -> (y <= 0)%Z.
+Lemma Zsgn_24 : forall x y : Z, (Z.sgn x + Z.sgn y < 0)%Z -> (y <= 0)%Z.
 Proof.
  intros [|p1|p1] [|p2|p2]; simpl in |- *;
   intros H H0; discriminate H || discriminate H0.
 Qed.
 
-Lemma Zsgn_25 : forall x : Z, Zsgn (- x) = (- Zsgn x)%Z.
+Lemma Zsgn_25 : forall x : Z, Z.sgn (- x) = (- Z.sgn x)%Z.
 Proof.
  intros [| p1| p1]; simpl in |- *; reflexivity.
 Qed.
 
 
-Lemma Zsgn_26 : forall x : Z, (0 < x)%Z -> (0 < Zsgn x)%Z.
+Lemma Zsgn_26 : forall x : Z, (0 < x)%Z -> (0 < Z.sgn x)%Z.
 Proof.
  intros [| p| p] Hp; trivial.
 Qed.
 
-Lemma Zsgn_27 : forall x : Z, (x < 0)%Z -> (Zsgn x < 0)%Z.
+Lemma Zsgn_27 : forall x : Z, (x < 0)%Z -> (Z.sgn x < 0)%Z.
 Proof.
  intros [| p| p] Hp; trivial.
 Qed.
@@ -1994,7 +1994,7 @@ Hint Resolve Zsgn_1 Zsgn_2 Zsgn_3 Zsgn_4 Zsgn_5 Zsgn_6 Zsgn_7 Zsgn_7' Zsgn_8
 (** Properties of Zabs                                                       *)
 (*###########################################################################*)
 
-Lemma Zabs_1 : forall z p : Z, (Zabs z < p)%Z -> (z < p)%Z /\ (- p < z)%Z.
+Lemma Zabs_1 : forall z p : Z, (Z.abs z < p)%Z -> (z < p)%Z /\ (- p < z)%Z.
 Proof.
  intros z p.
  case z.
@@ -2003,25 +2003,25 @@ Proof.
  split.
  assumption.
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
- replace (-1)%Z with (Zpred 0).
+ replace (-1)%Z with (Z.pred 0).
  apply Zlt_pred.
  simpl; trivial.
  ring_simplify (-1 * - p)%Z (-1 * 0)%Z.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
 
  intros.
  simpl in H.
  split.
  assumption.
- apply Zlt_trans with (m := 0%Z).
+ apply Z.lt_trans with (m := 0%Z).
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
- replace (-1)%Z with (Zpred 0).
+ replace (-1)%Z with (Z.pred 0).
  apply Zlt_pred.
  simpl; trivial.
  ring_simplify (-1 * - p)%Z (-1 * 0)%Z.
- apply Zlt_gt.
- apply Zlt_trans with (m := Zpos p0).
+ apply Z.lt_gt.
+ apply Z.lt_trans with (m := Zpos p0).
  constructor.
  assumption.
  constructor.
@@ -2029,28 +2029,28 @@ Proof.
  intros.
  simpl in H.
  split.
- apply Zlt_trans with (m := Zpos p0).
+ apply Z.lt_trans with (m := Zpos p0).
  constructor.
  assumption.
- 
+
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
- replace (-1)%Z with (Zpred 0).
+ replace (-1)%Z with (Z.pred 0).
  apply Zlt_pred.
  simpl;trivial.
  ring_simplify (-1 * - p)%Z.
  replace (-1 * Zneg p0)%Z with (- Zneg p0)%Z.
- replace (- Zneg p0)%Z with (Zpos p0). 
- apply Zlt_gt.
+ replace (- Zneg p0)%Z with (Zpos p0).
+ apply Z.lt_gt.
  assumption.
  symmetry  in |- *.
  apply Zopp_neg.
- rewrite Zopp_mult_distr_l_reverse with (n := 1%Z). 
+ rewrite Zopp_mult_distr_l_reverse with (n := 1%Z).
  simpl in |- *.
  constructor.
 Qed.
 
 
-Lemma Zabs_2 : forall z p : Z, (Zabs z > p)%Z -> (z > p)%Z \/ (- p > z)%Z.
+Lemma Zabs_2 : forall z p : Z, (Z.abs z > p)%Z -> (z > p)%Z \/ (- p > z)%Z.
 Proof.
  intros z p.
  case z.
@@ -2067,7 +2067,7 @@ Proof.
  intros.
  simpl in H.
  right.
- apply Zlt_gt.
+ apply Z.lt_gt.
  apply Zgt_mult_conv_absorb_l with (a := (-1)%Z).
  constructor.
  ring_simplify (-1 * - p)%Z.
@@ -2076,22 +2076,22 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zabs_3 : forall z p : Z, (z < p)%Z /\ (- p < z)%Z -> (Zabs z < p)%Z.
+Lemma Zabs_3 : forall z p : Z, (z < p)%Z /\ (- p < z)%Z -> (Z.abs z < p)%Z.
 Proof.
  intros z p.
  case z.
-  intro. 
+  intro.
   simpl in |- *.
   elim H.
   intros.
   assumption.
-  
+
   intros.
   elim H.
   intros.
   simpl in |- *.
   assumption.
-  
+
   intros.
   elim H.
   intros.
@@ -2100,14 +2100,14 @@ Proof.
   constructor.
   replace (-1 * Zpos p0)%Z with (Zneg p0).
   replace (-1 * p)%Z with (- p)%Z.
-  apply Zlt_gt.
+  apply Z.lt_gt.
   assumption.
-  ring.  
+  ring.
   simpl in |- *.
   reflexivity.
 Qed.
 
-Lemma Zabs_4 : forall z p : Z, (Zabs z < p)%Z -> (- p < z < p)%Z.
+Lemma Zabs_4 : forall z p : Z, (Z.abs z < p)%Z -> (- p < z < p)%Z.
 Proof.
  intros.
  split.
@@ -2118,28 +2118,28 @@ Proof.
  apply Zabs_1.
  assumption.
 Qed.
- 
 
-Lemma Zabs_5 : forall z p : Z, (Zabs z <= p)%Z -> (- p <= z <= p)%Z.
+
+Lemma Zabs_5 : forall z p : Z, (Z.abs z <= p)%Z -> (- p <= z <= p)%Z.
 Proof.
  intros.
  split.
- replace (- p)%Z with (Zsucc (- Zsucc p)).
+ replace (- p)%Z with (Z.succ (- Z.succ p)).
  apply Zlt_le_succ.
- apply proj2 with (A := (z < Zsucc p)%Z).
+ apply proj2 with (A := (z < Z.succ p)%Z).
  apply Zabs_1.
  apply Zle_lt_succ.
  assumption.
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  ring.
  apply Zlt_succ_le.
- apply proj1 with (B := (- Zsucc p < z)%Z).
+ apply proj1 with (B := (- Z.succ p < z)%Z).
  apply Zabs_1.
  apply Zle_lt_succ.
  assumption.
 Qed.
 
-Lemma Zabs_6 : forall z p : Z, (Zabs z <= p)%Z -> (z <= p)%Z.
+Lemma Zabs_6 : forall z p : Z, (Z.abs z <= p)%Z -> (z <= p)%Z.
 Proof.
  intros.
  apply proj2 with (A := (- p <= z)%Z).
@@ -2147,7 +2147,7 @@ Proof.
  assumption.
 Qed.
 
-Lemma Zabs_7 : forall z p : Z, (Zabs z <= p)%Z -> (- p <= z)%Z.
+Lemma Zabs_7 : forall z p : Z, (Z.abs z <= p)%Z -> (- p <= z)%Z.
 Proof.
  intros.
  apply proj1 with (B := (z <= p)%Z).
@@ -2155,7 +2155,7 @@ Proof.
  assumption.
 Qed.
 
-Lemma Zabs_8 : forall z p : Z, (- p <= z <= p)%Z -> (Zabs z <= p)%Z.
+Lemma Zabs_8 : forall z p : Z, (- p <= z <= p)%Z -> (Z.abs z <= p)%Z.
 Proof.
  intros.
  apply Zlt_succ_le.
@@ -2165,14 +2165,14 @@ Proof.
  split.
  apply Zle_lt_succ.
  assumption.
- apply Zlt_le_trans with (m := (- p)%Z).
- apply Zgt_lt. 
+ apply Z.lt_le_trans with (m := (- p)%Z).
+ apply Z.gt_lt.
  apply Zlt_opp.
  apply Zlt_succ.
  assumption.
 Qed.
 
-Lemma Zabs_min : forall z : Z, Zabs z = Zabs (- z).
+Lemma Zabs_min : forall z : Z, Z.abs z = Z.abs (- z).
 Proof.
  intro.
  case z.
@@ -2187,67 +2187,67 @@ Proof.
 Qed.
 
 Lemma Zabs_9 :
- forall z p : Z, (0 <= p)%Z -> (p < z)%Z \/ (z < - p)%Z -> (p < Zabs z)%Z.
+ forall z p : Z, (0 <= p)%Z -> (p < z)%Z \/ (z < - p)%Z -> (p < Z.abs z)%Z.
 Proof.
  intros.
  case H0.
  intro.
- replace (Zabs z) with z.
+ replace (Z.abs z) with z.
  assumption.
  symmetry  in |- *.
- apply Zabs_eq.
+ apply Z.abs_eq.
  apply Zlt_le_weak.
- apply Zle_lt_trans with (m := p).
+ apply Z.le_lt_trans with (m := p).
  assumption.
  assumption.
  intro.
- cut (Zabs z = (- z)%Z).
+ cut (Z.abs z = (- z)%Z).
  intro.
  rewrite H2.
  apply Zmin_cancel_Zlt.
  ring_simplify (- - z)%Z.
  assumption.
  rewrite Zabs_min.
- apply Zabs_eq.
+ apply Z.abs_eq.
  apply Zlt_le_weak.
- apply Zle_lt_trans with (m := p).
+ apply Z.le_lt_trans with (m := p).
  assumption.
  apply Zmin_cancel_Zlt.
  ring_simplify (- - z)%Z.
  assumption.
 Qed.
 
-Lemma Zabs_10 : forall z : Z, (0 <= Zabs z)%Z.
+Lemma Zabs_10 : forall z : Z, (0 <= Z.abs z)%Z.
 Proof.
  intro.
  case (Z_zerop z).
  intro.
  rewrite e.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  intro.
  case (not_Zeq z 0 n).
  intro.
  apply Zlt_le_weak.
  apply Zabs_9.
- apply Zle_refl.
+ apply Z.le_refl.
  simpl in |- *.
  right.
  assumption.
  intro.
  apply Zlt_le_weak.
  apply Zabs_9.
- apply Zle_refl.
+ apply Z.le_refl.
  simpl in |- *.
  left.
  assumption.
 Qed.
 
-Lemma Zabs_11 : forall z : Z, z <> 0%Z -> (0 < Zabs z)%Z.
+Lemma Zabs_11 : forall z : Z, z <> 0%Z -> (0 < Z.abs z)%Z.
 Proof.
  intros.
  apply Zabs_9.
- apply Zle_refl.
+ apply Z.le_refl.
  simpl in |- *.
  apply not_Zeq.
  intro.
@@ -2256,14 +2256,14 @@ Proof.
  assumption.
 Qed.
 
-Lemma Zabs_12 : forall z m : Z, (m < Zabs z)%Z -> {(m < z)%Z} + {(z < - m)%Z}.
+Lemma Zabs_12 : forall z m : Z, (m < Z.abs z)%Z -> {(m < z)%Z} + {(z < - m)%Z}.
 Proof.
  intros [| p| p] m; simpl in |- *; intros H;
-  [ left | left | right; apply Zmin_cancel_Zlt; rewrite Zopp_involutive ];
+  [ left | left | right; apply Zmin_cancel_Zlt; rewrite Z.opp_involutive ];
   assumption.
 Qed.
 
-Lemma Zabs_mult : forall z p : Z, Zabs (z * p) = (Zabs z * Zabs p)%Z.
+Lemma Zabs_mult : forall z p : Z, Z.abs (z * p) = (Z.abs z * Z.abs p)%Z.
 Proof.
  intros.
  case z.
@@ -2290,22 +2290,22 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zabs_plus : forall z p : Z, (Zabs (z + p) <= Zabs z + Zabs p)%Z.
+Lemma Zabs_plus : forall z p : Z, (Z.abs (z + p) <= Z.abs z + Z.abs p)%Z.
 Proof.
  intros.
  case z.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  case p.
  intro.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
- unfold Zabs at 2 in |- *.
- unfold Zabs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
  apply Zabs_8.
  split.
  apply Zplus_le_reg_l with (Zpos p1 - Zneg p0)%Z.
@@ -2322,17 +2322,17 @@ Proof.
  ring.
  ring.
  apply Zplus_le_compat.
- apply Zle_refl.
+ apply Z.le_refl.
  apply Zlt_le_weak.
  constructor.
- 
+
  case p.
  simpl in |- *.
  intro.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
- unfold Zabs at 2 in |- *.
- unfold Zabs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
+ unfold Z.abs at 2 in |- *.
  apply Zabs_8.
  split.
  apply Zplus_le_reg_l with (Zpos p1 + Zneg p0)%Z.
@@ -2360,13 +2360,13 @@ Proof.
  apply Zplus_le_compat.
  apply Zlt_le_weak.
  constructor.
- apply Zle_refl.
+ apply Z.le_refl.
  intros.
  simpl in |- *.
- apply Zle_refl.
+ apply Z.le_refl.
 Qed.
 
-Lemma Zabs_neg : forall z : Z, (z <= 0)%Z -> Zabs z = (- z)%Z.
+Lemma Zabs_neg : forall z : Z, (z <= 0)%Z -> Z.abs z = (- z)%Z.
 Proof.
  intro.
  case z.
@@ -2383,11 +2383,11 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Zle_Zabs: forall z, (z <= Zabs z)%Z.
+Lemma Zle_Zabs: forall z, (z <= Z.abs z)%Z.
 Proof.
- intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos. 
+ intros [|z|z]; simpl; auto with zarith; apply Zle_neg_pos.
 Qed.
- 
+
 Hint Resolve Zabs_1 Zabs_2 Zabs_3 Zabs_4 Zabs_5 Zabs_6 Zabs_7 Zabs_8 Zabs_9
   Zabs_10 Zabs_11 Zabs_12 Zabs_min Zabs_neg Zabs_mult Zabs_plus Zle_Zabs: zarith.
 
@@ -2400,7 +2400,7 @@ Lemma Zind :
  forall (P : Z -> Prop) (p : Z),
  P p ->
  (forall q : Z, (p <= q)%Z -> P q -> P (q + 1)%Z) ->
- forall q : Z, (p <= q)%Z -> P q. 
+ forall q : Z, (p <= q)%Z -> P q.
 Proof.
  intros P p.
  intro.
@@ -2426,14 +2426,14 @@ Proof.
  replace (p + Z_of_nat (S k))%Z with (p + k + 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (Z_of_nat 0). 
+ replace (- p + p)%Z with (Z_of_nat 0).
  ring_simplify (- p + (p + Z_of_nat k))%Z.
  apply Znat.inj_le.
  apply le_O_n.
- ring_simplify; auto with arith. 
+ ring_simplify; auto with arith.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  ring.
  intros.
  cut (exists k : nat, (q - p)%Z = Z_of_nat k).
@@ -2457,7 +2457,7 @@ Lemma Zrec :
  forall (P : Z -> Set) (p : Z),
  P p ->
  (forall q : Z, (p <= q)%Z -> P q -> P (q + 1)%Z) ->
- forall q : Z, (p <= q)%Z -> P q. 
+ forall q : Z, (p <= q)%Z -> P q.
 Proof.
  intros F p.
  intro.
@@ -2483,7 +2483,7 @@ Proof.
  replace (p + Z_of_nat (S k))%Z with (p + k + 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (Z_of_nat 0). 
+ replace (- p + p)%Z with (Z_of_nat 0).
  replace (- p + (p + Z_of_nat k))%Z with (Z_of_nat k).
  apply Znat.inj_le.
  apply le_O_n.
@@ -2491,7 +2491,7 @@ Proof.
  rewrite Zplus_opp_l; reflexivity.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  apply Zplus_assoc_reverse.
  intros.
  cut {k : nat | (q - p)%Z = Z_of_nat k}.
@@ -2540,14 +2540,14 @@ Proof.
  replace (p - 0)%Z with p.
  assumption.
  unfold Zminus in |- *.
- unfold Zopp in |- *.
+ unfold Z.opp in |- *.
  rewrite Zplus_0_r; reflexivity.
  replace (p - Z_of_nat (S k))%Z with (p - k - 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (- Z_of_nat 0)%Z. 
+ replace (- p + p)%Z with (- Z_of_nat 0)%Z.
  replace (- p + (p - Z_of_nat k))%Z with (- Z_of_nat k)%Z.
- apply Zge_le.
+ apply Z.ge_le.
  apply Zge_opp.
  apply Znat.inj_le.
  apply le_O_n.
@@ -2555,7 +2555,7 @@ Proof.
  rewrite Zplus_opp_l; reflexivity.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  unfold Zminus at 1 2 in |- *.
  rewrite Zplus_assoc_reverse.
  rewrite <- Zopp_plus_distr.
@@ -2567,16 +2567,16 @@ Proof.
  intro k.
  intros.
  exists k.
- apply Zopp_inj. 
+ apply Z.opp_inj.
  apply Zplus_reg_l with (n := p).
- replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k). 
+ replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k).
  rewrite <- e.
  reflexivity.
  unfold Zminus in |- *.
  rewrite Zopp_plus_distr.
  rewrite Zplus_assoc.
  rewrite Zplus_opp_r.
- rewrite Zopp_involutive.
+ rewrite Z.opp_involutive.
  reflexivity.
  apply Z_of_nat_complete_inf.
  unfold Zminus in |- *.
@@ -2615,17 +2615,17 @@ Proof.
  replace (p - Z_of_nat (S k))%Z with (p - k - 1)%Z.
  apply H0.
  apply Zplus_le_reg_l with (p := (- p)%Z).
- replace (- p + p)%Z with (- Z_of_nat 0)%Z. 
+ replace (- p + p)%Z with (- Z_of_nat 0)%Z.
  replace (- p + (p - Z_of_nat k))%Z with (- Z_of_nat k)%Z.
- apply Zge_le.
+ apply Z.ge_le.
  apply Zge_opp.
  apply Znat.inj_le.
  apply le_O_n.
- ring. 
+ ring.
  ring_simplify; auto with arith.
  assumption.
  rewrite (Znat.inj_S k).
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  ring.
  intros.
  cut (exists k : nat, (p - q)%Z = Z_of_nat k).
@@ -2634,9 +2634,9 @@ Proof.
  intro k.
  intros.
  exists k.
- apply Zopp_inj. 
+ apply Z.opp_inj.
  apply Zplus_reg_l with (n := p).
- replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k). 
+ replace (p + - (p - Z_of_nat k))%Z with (Z_of_nat k).
  rewrite <- H3.
  ring.
  ring.
@@ -2654,44 +2654,44 @@ Proof.
  intros P p WF_ind_step q Hq.
  cut (forall x : Z, (p <= x)%Z -> forall y : Z, (p <= y < x)%Z -> P y).
  intro.
- apply (H (Zsucc q)).
+ apply (H (Z.succ q)).
  apply Zle_le_succ.
  assumption.
- 
+
  split; [ assumption | exact (Zlt_succ q) ].
 
- intros x0 Hx0; generalize Hx0; pattern x0 in |- *. 
+ intros x0 Hx0; generalize Hx0; pattern x0 in |- *.
  apply Zrec with (p := p).
  intros.
  absurd (p <= p)%Z.
  apply Zgt_not_le.
  apply Zgt_le_trans with (m := y).
- apply Zlt_gt.
+ apply Z.lt_gt.
  elim H.
  intros.
  assumption.
  elim H.
  intros.
  assumption.
- apply Zle_refl.
+ apply Z.le_refl.
 
- intros. 
- apply WF_ind_step. 
+ intros.
+ apply WF_ind_step.
  intros.
  apply (H0 H).
- split. 
+ split.
  elim H2.
  intros.
  assumption.
- apply Zlt_le_trans with y. 
+ apply Z.lt_le_trans with y.
  elim H2.
  intros.
  assumption.
- apply Zgt_succ_le. 
- apply Zlt_gt. 
+ apply Zgt_succ_le.
+ apply Z.lt_gt.
  elim H1.
  intros.
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  assumption.
  assumption.
 Qed.
@@ -2744,44 +2744,44 @@ Proof.
  intros P p WF_ind_step q Hq.
  cut (forall x : Z, (p <= x)%Z -> forall y : Z, (p <= y < x)%Z -> P y).
  intro.
- apply (H (Zsucc q)).
+ apply (H (Z.succ q)).
  apply Zle_le_succ.
  assumption.
- 
+
  split; [ assumption | exact (Zlt_succ q) ].
 
- intros x0 Hx0; generalize Hx0; pattern x0 in |- *. 
+ intros x0 Hx0; generalize Hx0; pattern x0 in |- *.
  apply Zind with (p := p).
  intros.
  absurd (p <= p)%Z.
  apply Zgt_not_le.
  apply Zgt_le_trans with (m := y).
- apply Zlt_gt.
+ apply Z.lt_gt.
  elim H.
  intros.
  assumption.
  elim H.
  intros.
  assumption.
- apply Zle_refl.
+ apply Z.le_refl.
 
- intros. 
- apply WF_ind_step. 
+ intros.
+ apply WF_ind_step.
  intros.
  apply (H0 H).
- split. 
+ split.
  elim H2.
  intros.
  assumption.
- apply Zlt_le_trans with y. 
+ apply Z.lt_le_trans with y.
  elim H2.
  intros.
  assumption.
- apply Zgt_succ_le. 
- apply Zlt_gt. 
+ apply Zgt_succ_le.
+ apply Z.lt_gt.
  elim H1.
  intros.
- unfold Zsucc in |- *.
+ unfold Z.succ in |- *.
  assumption.
  assumption.
 Qed.
@@ -2830,16 +2830,16 @@ Qed.
 (** Properties of Zmax                                                       *)
 (*###########################################################################*)
 
-Definition Zmax (n m : Z) := (n + m - Zmin n m)%Z.
+Definition Zmax (n m : Z) := (n + m - Z.min n m)%Z.
 
 Lemma ZmaxSS : forall n m : Z, (Zmax n m + 1)%Z = Zmax (n + 1) (m + 1).
 Proof.
  intros.
  unfold Zmax in |- *.
- replace (Zmin (n + 1) (m + 1)) with (Zmin n m + 1)%Z.
+ replace (Z.min (n + 1) (m + 1)) with (Z.min n m + 1)%Z.
  ring.
  symmetry  in |- *.
- change (Zmin (Zsucc n) (Zsucc m) = Zsucc (Zmin n m)) in |- *.
+ change (Z.min (Z.succ n) (Z.succ m) = Z.succ (Z.min n m)) in |- *.
  symmetry  in |- *.
  apply Zmin_SS.
 Qed.
@@ -2848,29 +2848,29 @@ Lemma Zle_max_l : forall n m : Z, (n <= Zmax n m)%Z.
 Proof.
  intros.
  unfold Zmax in |- *.
- apply Zplus_le_reg_l with (p := (- n + Zmin n m)%Z).
- ring_simplify (- n + Zmin n m + n)%Z.
- ring_simplify (- n + Zmin n m + (n + m - Zmin n m))%Z.
- apply Zle_min_r.
+ apply Zplus_le_reg_l with (p := (- n + Z.min n m)%Z).
+ ring_simplify (- n + Z.min n m + n)%Z.
+ ring_simplify (- n + Z.min n m + (n + m - Z.min n m))%Z.
+ apply Z.le_min_r.
 Qed.
 
 Lemma Zle_max_r : forall n m : Z, (m <= Zmax n m)%Z.
 Proof.
  intros.
  unfold Zmax in |- *.
- apply Zplus_le_reg_l with (p := (- m + Zmin n m)%Z).
- ring_simplify (- m + Zmin n m + m)%Z.
- ring_simplify (- m + Zmin n m + (n + m - Zmin n m))%Z.
- apply Zle_min_l.
+ apply Zplus_le_reg_l with (p := (- m + Z.min n m)%Z).
+ ring_simplify (- m + Z.min n m + m)%Z.
+ ring_simplify (- m + Z.min n m + (n + m - Z.min n m))%Z.
+ apply Z.le_min_l.
 Qed.
 
 
-Lemma Zmin_or_informative : forall n m : Z, {Zmin n m = n} + {Zmin n m = m}.
+Lemma Zmin_or_informative : forall n m : Z, {Z.min n m = n} + {Z.min n m = m}.
 Proof.
  intros.
  case (Z_lt_ge_dec n m).
- unfold Zmin in |- *.
- unfold Zlt in |- *.
+ unfold Z.min in |- *.
+ unfold Z.lt in |- *.
  intro z.
  rewrite z.
  left.
@@ -2880,8 +2880,8 @@ Proof.
  intro.
  case H.
  intros z0.
- unfold Zmin in |- *.
- unfold Zgt in z0.
+ unfold Z.min in |- *.
+ unfold Z.gt in z0.
  rewrite z0.
  right.
  reflexivity.
@@ -2894,14 +2894,14 @@ Proof.
  elim H.
  intro.
  left.
- apply Zlt_gt.
+ apply Z.lt_gt.
  assumption.
  intro.
  right.
  symmetry  in |- *.
  assumption.
- apply Z_le_lt_eq_dec. 
- apply Zge_le.
+ apply Z_le_lt_eq_dec.
+ apply Z.ge_le.
  assumption.
 Qed.
 
@@ -2925,8 +2925,8 @@ Proof.
  assumption.
  ring.
 Qed.
- 
-Lemma Zmax_or_informative : forall n m : Z, {Zmax n m = n} + {Zmax n m = m}. 
+
+Lemma Zmax_or_informative : forall n m : Z, {Zmax n m = n} + {Zmax n m = m}.
 Proof.
  intros.
  unfold Zmax in |- *.
@@ -2960,12 +2960,12 @@ Proof.
  exact Zeven.Zeven_Sn.
 Qed.
 
-Lemma Zeven_pred : forall x : Z, Zeven.Zodd x -> Zeven.Zeven (x - 1). 
+Lemma Zeven_pred : forall x : Z, Zeven.Zodd x -> Zeven.Zeven (x - 1).
 Proof.
  exact Zeven.Zeven_pred.
 Qed.
 
-(* This lemma used to be useful since it was mentioned with an unnecessary premise 
+(* This lemma used to be useful since it was mentioned with an unnecessary premise
    `x>=0` as Z_modulo_2 in ZArith, but the ZArith version has been fixed. *)
 
 Definition Z_modulo_2_always :
@@ -2987,10 +2987,10 @@ Proof.
 Qed.
 
 Lemma Z_div_le :
- forall a b c : Z, (0 < c)%Z -> (b <= a)%Z -> (b / c <= a / c)%Z. 
+ forall a b c : Z, (0 < c)%Z -> (b <= a)%Z -> (b / c <= a / c)%Z.
 Proof.
  intros.
- apply Zge_le.
+ apply Z.ge_le.
  apply Z_div_ge; Flip; assumption.
 Qed.
 
@@ -2998,7 +2998,7 @@ Lemma Z_div_nonneg :
  forall a b : Z, (0 < b)%Z -> (0 <= a)%Z -> (0 <= a / b)%Z.
 Proof.
  intros.
- apply Zge_le.
+ apply Z.ge_le.
  apply Z_div_ge0; Flip; assumption.
 Qed.
 
@@ -3012,7 +3012,7 @@ Proof.
  intro.
  apply (Zlt_not_le (b * (a / b) + a mod b) 0 H0).
  apply Zplus_le_0_compat.
- apply Zmult_le_0_compat. 
+ apply Zmult_le_0_compat.
  apply Zlt_le_weak; assumption.
  Flip.
  assumption.
diff --git a/test-suite/success/Case11.v b/test-suite/success/Case11.v
index 445ffac8cb..fbe909ec41 100644
--- a/test-suite/success/Case11.v
+++ b/test-suite/success/Case11.v
@@ -5,9 +5,9 @@ Section A.
 
 Variables (Alpha : Set) (Beta : Set).
 
-Definition nodep_prod_of_dep (c : sigS (fun a : Alpha => Beta)) :
+Definition nodep_prod_of_dep (c : sigT (fun a : Alpha => Beta)) :
   Alpha * Beta := match c with
-                  | existS _ a b => (a, b)
+                  | existT _ a b => (a, b)
                   end.
 
 End A.
diff --git a/test-suite/success/Case17.v b/test-suite/success/Case17.v
index 861d04668f..a4efcca945 100644
--- a/test-suite/success/Case17.v
+++ b/test-suite/success/Case17.v
@@ -1,5 +1,5 @@
 (* Check the synthesis of predicate from a cast in case of matching of
-   the first component (here [list bool]) of a dependent type (here [sigS])
+   the first component (here [list bool]) of a dependent type (here [sigT])
    (Simplification of an example from file parsing2.v of the Coq'Art
     exercises) *)
 
@@ -19,10 +19,10 @@ Axiom HHH : forall A : Prop, A.
 
 Check
   (match rec l0 (HHH _) with
-   | inleft (existS _ (false :: l1) _) => inright _ (HHH _)
-   | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
+   | inleft (existT _ (false :: l1) _) => inright _ (HHH _)
+   | inleft (existT _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
        inright _ (HHH _)
-   | inleft (existS _ _ _) => inright _ (HHH _)
+   | inleft (existT _ _ _) => inright _ (HHH _)
    | inright Hnp => inright _ (HHH _)
    end
    :{l'' : list bool &
@@ -39,10 +39,10 @@ Check
             {t : nat | parse_rel l' l'' t /\ length l'' <= length l'}} +
             {(forall (l'' : list bool) (t : nat), ~ parse_rel l' l'' t)}) =>
    match rec l0 (HHH _) with
-   | inleft (existS _ (false :: l1) _) => inright _ (HHH _)
-   | inleft (existS _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
+   | inleft (existT _ (false :: l1) _) => inright _ (HHH _)
+   | inleft (existT _ (true :: l1) (exist _ t1 (conj Hp Hl))) =>
        inright _ (HHH _)
-   | inleft (existS _ _ _) => inright _ (HHH _)
+   | inleft (existT _ _ _) => inright _ (HHH _)
    | inright Hnp => inright _ (HHH _)
    end
    :{l'' : list bool &
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 288c9d1da0..5650dba236 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq88.
+Import Coq.Compat.Coq89.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index b7bbc505b4..37d50ee67d 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq89.
 Import Coq.Compat.Coq88.
 Import Coq.Compat.Coq87.
-Import Coq.Compat.Coq86.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index 9cfe60390f..9981388381 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.7") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq89.
 Import Coq.Compat.Coq88.
-Import Coq.Compat.Coq87.
diff --git a/test-suite/success/FunindExtraction_compat86.v b/test-suite/success/FunindExtraction_compat86.v
deleted file mode 100644
index 8912197d2f..0000000000
--- a/test-suite/success/FunindExtraction_compat86.v
+++ /dev/null
@@ -1,506 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.6") -*- *)
-
-Definition iszero (n : nat) : bool :=
-  match n with
-  | O => true
-  | _ => false
-  end.
-
-Functional Scheme iszero_ind := Induction for iszero Sort Prop.
-
-Lemma toto : forall n : nat, n = 0 -> iszero n = true.
-intros x eg.
- functional induction iszero x; simpl.
-trivial.
-inversion eg.
-Qed.
-
-
-Function ftest (n m : nat) : nat :=
-  match n with
-  | O => match m with
-         | O => 0
-         | _ => 1
-         end
-  | S p => 0
-  end.
-(* MS: FIXME: apparently can't define R_ftest_complete. Rest of the file goes through. *)
-
-Lemma test1 : forall n m : nat, ftest n m <= 2.
-intros n m.
- functional induction ftest n m; auto.
-Qed.
-
-Lemma test2 : forall m n, ~ 2 = ftest n m.
-Proof.
-intros n m;intro H.
-functional inversion H ftest.
-Qed.
-
-Lemma test3 : forall n m, ftest n m = 0 -> (n = 0 /\ m = 0)  \/ n <> 0.
-Proof.
-functional inversion 1 ftest;auto.
-Qed.
-
-
-Require Import Arith.
-Lemma test11 : forall m : nat, ftest 0 m <= 2.
-intros m.
- functional induction ftest 0 m.
-auto.
-auto.
-auto with *.
-Qed.
-
-Function lamfix (m n : nat) {struct n } : nat :=
-  match n with
-    | O => m
-    | S p => lamfix m p
-  end.
-
-(* Parameter v1 v2 : nat. *)
-
-Lemma lamfix_lem : forall v1 v2 : nat, lamfix v1 v2 = v1.
-intros v1 v2.
- functional induction lamfix v1 v2.
-trivial.
-assumption.
-Defined.
-
-
-
-(* polymorphic function *)
-Require Import List.
-
-Functional Scheme app_ind := Induction for app Sort Prop.
-
-Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
-intros A l l'.
- functional induction app A l l';  intuition.
- rewrite <- H0; trivial.
-Qed.
-
-
-
-
-
-Require Export Arith.
-
-
-Function trivfun (n : nat) : nat :=
-  match n with
-  | O => 0
-  | S m => trivfun m
-  end.
-
-
-(* essaie de parametre variables non locaux:*)
-
-Parameter varessai : nat.
-
-Lemma first_try : trivfun varessai = 0.
- functional induction trivfun varessai.
-trivial.
-assumption.
-Defined.
-
-
- Functional Scheme triv_ind := Induction for trivfun Sort Prop.
-
-Lemma bisrepetita : forall n' : nat, trivfun n' = 0.
-intros n'.
- functional induction trivfun n'.
-trivial.
-assumption.
-Qed.
-
-
-
-
-
-
-
-Function iseven (n : nat) : bool :=
-  match n with
-  | O => true
-  | S (S m) => iseven m
-  | _ => false
-  end.
-
-
-Function funex (n : nat) : nat :=
-  match iseven n with
-  | true => n
-  | false => match n with
-             | O => 0
-             | S r => funex r
-             end
-  end.
-
-
-Function nat_equal_bool (n m : nat) {struct n} : bool :=
-  match n with
-  | O => match m with
-         | O => true
-         | _ => false
-         end
-  | S p => match m with
-           | O => false
-           | S q => nat_equal_bool p q
-           end
-  end.
-
-
-Require Export Div2.
-Require Import Nat.
-Functional Scheme div2_ind := Induction for div2 Sort Prop.
-Lemma div2_inf : forall n : nat, div2 n <= n.
-intros n.
- functional induction div2 n.
-auto.
-auto.
-
-apply le_S.
-apply le_n_S.
-exact IHn0.
-Qed.
-
-(* reuse this lemma as a scheme:*)
-
-Function nested_lam (n : nat) : nat -> nat :=
-  match n with
-  | O => fun m : nat => 0
-  | S n' => fun m : nat => m + nested_lam n' m
-  end.
-
-
-Lemma nest : forall n m : nat, nested_lam n m = n * m.
-intros n m.
- functional induction nested_lam n m; simpl;auto.
-Qed.
-
-
-Function essai (x : nat) (p : nat * nat) {struct x} : nat :=
-  let (n, m) := (p: nat*nat) in
-  match n with
-  | O => 0
-  | S q => match x with
-           | O => 1
-           | S r => S (essai r (q, m))
-           end
-  end.
-
-Lemma essai_essai :
- forall (x : nat) (p : nat * nat), let (n, m) := p in 0 < n -> 0 < essai x p.
-intros x p.
- functional induction essai x p; intros.
-inversion H.
-auto with arith.
- auto with arith.
-Qed.
-
-Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
-  let x := nat_equal_bool m 5 in
-  let y := 0 in
-  match n with
-  | O => y
-  | S q =>
-      let recapp := plus_x_not_five'' q m in
-      match x with
-      | true => S recapp
-      | false => S recapp
-      end
-  end.
-
-Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
-intros a b.
- functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
-Qed.
-
-Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
-intros n m.
- functional induction nat_equal_bool n m; simpl; intros hyp; auto.
-rewrite <- hyp in y; simpl in y;tauto.
-inversion hyp.
-Qed.
-
-Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
-intros n m.
- functional induction nat_equal_bool n m; simpl; intros eg; auto.
-inversion eg.
-inversion eg.
-Qed.
-
-
-Inductive istrue : bool -> Prop :=
-    istrue0 : istrue true.
-
-Functional Scheme add_ind := Induction for add Sort Prop.
-
-Lemma inf_x_plusxy' : forall x y : nat, x <= x + y.
-intros n m.
- functional induction add n m; intros.
-auto with arith.
-auto with arith.
-Qed.
-
-
-Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
-intros n.
-unfold plus.
- functional induction plus n 0; intros.
-auto with arith.
-apply le_n_S.
-assumption.
-Qed.
-
-Lemma inf_x_plusxy''' : forall x : nat, x <= 0 + x.
-intros n.
- functional induction plus 0 n; intros; auto with arith.
-Qed.
-
-Function mod2 (n : nat) : nat :=
-  match n with
-  | O => 0
-  | S (S m) => S (mod2 m)
-  | _ => 0
-  end.
-
-Lemma princ_mod2 : forall n : nat, mod2 n <= n.
-intros n.
- functional induction mod2 n; simpl; auto with arith.
-Qed.
-
-Function isfour (n : nat) : bool :=
-  match n with
-  | S (S (S (S O))) => true
-  | _ => false
-  end.
-
-Function isononeorfour (n : nat) : bool :=
-  match n with
-  | S O => true
-  | S (S (S (S O))) => true
-  | _ => false
-  end.
-
-Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
-intros n.
- functional induction isononeorfour n; intros istr; simpl;
- inversion istr.
-apply istrue0.
-destruct n. inversion istr.
-destruct n. tauto.
-destruct n. inversion istr.
-destruct n. inversion istr.
-destruct n. tauto.
-simpl in *. inversion H0.
-Qed.
-
-Lemma toto' : forall n m : nat, n = 4 -> istrue (isononeorfour n).
-intros n.
- functional induction isononeorfour n; intros m istr; inversion istr.
-apply istrue0.
-rewrite H in y; simpl in y;tauto.
-Qed.
-
-Function ftest4 (n m : nat) : nat :=
-  match n with
-  | O => match m with
-         | O => 0
-         | S q => 1
-         end
-  | S p => match m with
-           | O => 0
-           | S r => 1
-           end
-  end.
-
-Lemma test4 : forall n m : nat, ftest n m <= 2.
-intros n m.
- functional induction ftest n m; auto with arith.
-Qed.
-
-Lemma test4' : forall n m : nat, ftest4 (S n) m <= 2.
-intros n m.
-assert ({n0 | n0 = S n}).
-exists (S n);reflexivity.
-destruct H as [n0 H1].
-rewrite <- H1;revert H1.
- functional induction ftest4 n0 m.
-inversion 1.
-inversion 1.
-
-auto with arith.
-auto with arith.
-Qed.
-
-Function ftest44 (x : nat * nat) (n m : nat) : nat :=
-  let (p, q) := (x: nat*nat) in
-  match n with
-  | O => match m with
-         | O => 0
-         | S q => 1
-         end
-  | S p => match m with
-           | O => 0
-           | S r => 1
-           end
-  end.
-
-Lemma test44 :
- forall (pq : nat * nat) (n m o r s : nat), ftest44 pq n (S m) <= 2.
-intros pq n m o r s.
- functional induction ftest44 pq n (S m).
-auto with arith.
-auto with arith.
-auto with arith.
-auto with arith.
-Qed.
-
-Function ftest2 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => match m with
-         | O => 0
-         | S q => 0
-         end
-  | S p => ftest2 p m
-  end.
-
-Lemma test2' : forall n m : nat, ftest2 n m <= 2.
-intros n m.
- functional induction ftest2 n m; simpl; intros; auto.
-Qed.
-
-Function ftest3 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => 0
-  | S p => match m with
-           | O => ftest3 p 0
-           | S r => 0
-           end
-  end.
-
-Lemma test3' : forall n m : nat, ftest3 n m <= 2.
-intros n m.
- functional induction ftest3 n m.
-intros.
-auto.
-intros.
-auto.
-intros.
-simpl.
-auto.
-Qed.
-
-Function ftest5 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => 0
-  | S p => match m with
-           | O => ftest5 p 0
-           | S r => ftest5 p r
-           end
-  end.
-
-Lemma test5 : forall n m : nat, ftest5 n m <= 2.
-intros n m.
- functional induction ftest5 n m.
-intros.
-auto.
-intros.
-auto.
-intros.
-simpl.
-auto.
-Qed.
-
-Function ftest7 (n : nat) : nat :=
-  match ftest5 n 0 with
-  | O => 0
-  | S r => 0
-  end.
-
-Lemma essai7 :
- forall (Hrec : forall n : nat, ftest5 n 0 = 0 -> ftest7 n <= 2)
-   (Hrec0 : forall n r : nat, ftest5 n 0 = S r -> ftest7 n <= 2)
-   (n : nat), ftest7 n <= 2.
-intros hyp1 hyp2 n.
- functional induction ftest7 n; auto.
-Qed.
-
-Function ftest6 (n m : nat) {struct n} : nat :=
-  match n with
-  | O => 0
-  | S p => match ftest5 p 0 with
-           | O => ftest6 p 0
-           | S r => ftest6 p r
-           end
-  end.
-
-
-Lemma princ6 :
- (forall n m : nat, n = 0 -> ftest6 0 m <= 2) ->
- (forall n m p : nat,
-  ftest6 p 0 <= 2 -> ftest5 p 0 = 0 -> n = S p -> ftest6 (S p) m <= 2) ->
- (forall n m p r : nat,
-  ftest6 p r <= 2 -> ftest5 p 0 = S r -> n = S p -> ftest6 (S p) m <= 2) ->
- forall x y : nat, ftest6 x y <= 2.
-intros hyp1 hyp2 hyp3 n m.
-generalize hyp1 hyp2 hyp3.
-clear hyp1 hyp2 hyp3.
- functional induction ftest6 n m; auto.
-Qed.
-
-Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
-intros n m.
- functional induction ftest6 n m; simpl; auto.
-Qed.
-
-(* Some tests with modules *)
-Module M.
-Function test_m (n:nat) : nat :=
-  match n with
-    | 0 => 0
-    | S n =>  S (S (test_m n))
-  end.
-
-Lemma test_m_is_double :  forall n, div2 (test_m n) = n.
-Proof.
-intros n.
-functional induction (test_m n).
-reflexivity.
-simpl;rewrite IHn0;reflexivity.
-Qed.
-End M.
-(* We redefine a new Function with the same name *)
-Function test_m (n:nat) : nat :=
-  pred n.
-
-Lemma test_m_is_pred : forall n, test_m n = pred n.
-Proof.
-intro n.
-functional induction (test_m n). (* the test_m_ind to use is the last defined  saying that test_m = pred*)
-reflexivity.
-Qed.
-
-(* Checks if the dot notation are correctly treated in infos *)
-Lemma M_test_m_is_double : forall n, div2 (M.test_m n) = n.
-intro n.
-(* here we should apply M.test_m_ind *)
-functional induction (M.test_m n).
-reflexivity.
-simpl;rewrite IHn0;reflexivity.
-Qed.
-
-Import M.
-(* Now test_m is the one which defines double *)
-
-Lemma test_m_is_double : forall n, div2 (M.test_m n) = n.
-intro n.
-(* here we should apply M.test_m_ind *)
-functional induction (test_m n).
-reflexivity.
-simpl;rewrite IHn0;reflexivity.
-Qed.
-
-Extraction iszero.
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 78652fb64b..7ee471bae7 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -19,8 +19,8 @@ Qed.
 (* Check that no tuple needs to be built *)
 Lemma l3 :
  forall x y : nat,
- existS (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
- existS (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
+ existT (fun n : nat => {n = n} + {n = n}) x (left _ (refl_equal x)) =
+ existT (fun n : nat => {n = n} + {n = n}) y (left _ (refl_equal y)) ->
  x = y.
 intros x y H.
  injection H.
@@ -30,10 +30,10 @@ Qed.
 (* Check that a tuple is built (actually the same as the initial one) *)
 Lemma l4 :
  forall p1 p2 : {0 = 0} + {0 = 0},
- existS (fun n : nat => {n = n} + {n = n}) 0 p1 =
- existS (fun n : nat => {n = n} + {n = n}) 0 p2 ->
- existS (fun n : nat => {n = n} + {n = n}) 0 p1 =
- existS (fun n : nat => {n = n} + {n = n}) 0 p2.
+ existT (fun n : nat => {n = n} + {n = n}) 0 p1 =
+ existT (fun n : nat => {n = n} + {n = n}) 0 p2 ->
+ existT (fun n : nat => {n = n} + {n = n}) 0 p1 =
+ existT (fun n : nat => {n = n} + {n = n}) 0 p2.
 intros.
  injection H.
 exact (fun H => H).
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 448d0082db..baf089796f 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -7,7 +7,7 @@ Inductive listn : nat -> Set :=
 Axiom
   ax :
     forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
-    existS _ (n + n') l = existS _ (n' + n) l'.
+    existT _ (n + n') l = existT _ (n' + n) l'.
 
 Lemma lem :
  forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
@@ -72,7 +72,7 @@ Qed.
 
 Require Import JMeq.
 
-Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True.  
+Goal forall A B (a:A) (b:B), JMeq a b -> JMeq b a -> True.
 inversion 1; (* Goal is now [JMeq a a -> True] *) dependent rewrite H3.
 Undo.
 intros; inversion H; dependent rewrite H4 in H0.
@@ -135,7 +135,7 @@ Abort.
 Goal forall x y, x=y+0 -> let z := x+1 in x+1=y -> z=z -> z=x.
 intros.
 subst x. (* was failing *)
-subst z. 
+subst z.
 rewrite H0.
 auto with arith.
 Qed.
diff --git a/theories/Compat/Coq88.v b/theories/Compat/Coq88.v
index 578425bfb5..950cd8242b 100644
--- a/theories/Compat/Coq88.v
+++ b/theories/Compat/Coq88.v
@@ -9,6 +9,8 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.8 *)
+Require Export Coq.Compat.Coq89.
+
 (** In Coq 8.9, prim token notations follow [Import] rather than
     [Require].  So we make all of the relevant notations accessible in
     compatibility mode. *)
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq89.v
index 666be207eb..d25671887f 100644
--- a/theories/Compat/Coq86.v
+++ b/theories/Compat/Coq89.v
@@ -8,8 +8,4 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Compatibility file for making Coq act similar to Coq v8.6 *)
-Require Export Coq.Compat.Coq87.
-
-Require Export Coq.extraction.Extraction.
-Require Export Coq.funind.FunInd.
+(** Compatibility file for making Coq act similar to Coq v8.9 *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 1baaa8a45f..06d9ba3436 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -152,9 +152,9 @@ let add_vo_require opts d p export =
 
 let add_compat_require opts v =
   match v with
-  | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false)
   | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
-  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
+  | Flags.V8_8 -> add_vo_require opts "Coq.Compat.Coq88" None (Some false)
+  | Flags.Current -> add_vo_require opts "Coq.Compat.Coq89" None (Some false)
 
 let set_batch_mode opts =
   Flags.quiet := true;
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 7dd5471f3f..cf69a84b8b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -60,10 +60,10 @@ let make_bullet s =
   | _ -> assert false
 
 let parse_compat_version = let open Flags in function
-  | "8.8" -> Current
+  | "8.9" -> Current
+  | "8.8" -> V8_8
   | "8.7" -> V8_7
-  | "8.6" -> V8_6
-  | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+  | ("8.6" | "8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->