ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7

22 files changed, 90 insertions, 90 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 495a16bca..ee9e2504a 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -26,13 +26,13 @@ Program Fixpoint union
     | t1,Leaf => t1
     | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
         if (Z_ge_lt_dec h1 h2) then
-          if (Z_eq_dec h2 1)
+          if (Z.eq_dec h2 1)
           then add v2 s
           else
             let (l2', r2') := split v1 u in
             join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
         else
-          if (Z_eq_dec h1 1)
+          if (Z.eq_dec h1 1)
           then add v1 s
           else
             let (l1', r1') := split v2 u in
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 718b0e861..fb2f0ca90 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,7 +58,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
   match x with
     | I x =>
       match y with
-        | I y => if (Z_eq_dec x y) then in_left else in_right
+        | I y => if (Z.eq_dec x y) then in_left else in_right
         | S ys => in_right
       end
     | S xs =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 5627612f6..17eeb3529 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -1,6 +1,6 @@
 Require Import ZArith.
 
-Definition zeq := Z_eq_dec.
+Definition zeq := Z.eq_dec.
 
 Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
  fun y => if zeq x y then v else s y.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 72396d490..d58376198 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -13,7 +13,7 @@ Qed.
 
 Require Import ZArith.
 
-Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt.
 
 Lemma f_refl'' : forall n , f'' true n n.
 Proof.
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 0fc854b6f..142ada268 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -1,8 +1,8 @@
-(* Check that "apply refl_equal" is not exported as an interactive
+(* Check that "apply eq_refl" is not exported as an interactive
    tactic but as a statically globalized one *)
 
 (* (this is a simplification of the original bug report) *)
 
 Module A.
-Hint Rewrite sym_equal using apply refl_equal : foo.
+Hint Rewrite eq_sym using apply eq_refl : foo.
 End A.
diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index 6945edc88..c3634f640 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -3,7 +3,7 @@
 
 Require Import BinInt Zbool.
 
-Definition Zplus x y :=
+Definition Z.add x y :=
 match x with
 | 0%Z => y
 | Zpos x' =>
@@ -32,7 +32,7 @@ end.
 
 Require Import Ring.
 
-Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z).
+Lemma Zth : ring_theory Z0 (Zpos xH) Z.add Z.mul Z.sub Z.opp (@eq Z).
 Admitted.
 
 Ltac Zcst t :=
@@ -45,7 +45,7 @@ Add Ring Zr : Zth
   (decidable Zeq_bool_eq, constants [Zcst]).
 
 Open Scope Z_scope.
-Infix "+" := Zplus : Z_scope.
+Infix "+" := Z.add : Z_scope.
 
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
 Timeout 5 Time intro; ring.
diff --git a/test-suite/ideal-features/eapply_evar.v b/test-suite/ideal-features/eapply_evar.v
index 547860bf1..bb61afb88 100644
--- a/test-suite/ideal-features/eapply_evar.v
+++ b/test-suite/ideal-features/eapply_evar.v
@@ -4,6 +4,6 @@
    and not "O = O" *)
 
 Lemma eapply_evar : O=O -> 0=O.
-intro H; eapply trans_equal;
+intro H; eapply eq_trans;
   [apply H | match goal with |- ?x = ?x => reflexivity end].
 Qed.
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index f5a953566..4a1231b35 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -77,13 +77,13 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop :=
 
 Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t  /\ correct q t /\
   rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  ->
-  Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s).
+  Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s).
 Proof.
   intros.
-  generalize (Zabs_eq (C p t - D q t)).
-  generalize (Zabs_non_eq (C p t - D q t)).
-  generalize (Zabs_eq (C p s -D q s)).
-  generalize (Zabs_non_eq (C p s - D q s)).
+  generalize (Z.abs_eq (C p t - D q t)).
+  generalize (Z.abs_neq (C p t - D q t)).
+  generalize (Z.abs_eq (C p s -D q s)).
+  generalize (Z.abs_neq (C p s - D q s)).
   unfold rbound2 in H.
   unfold rbound1 in H.
   intuition.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 4c00ffe4a..6fa547358 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -9,17 +9,17 @@
 Require Import ZArith Zwf Psatz QArith.
 Open Scope Z_scope.
 
-Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
+Lemma Z.abs_square : forall x,  (Z.abs  x)^2 = x^2.
 Proof.
  intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
 Qed.
-Hint Resolve Zabs_pos Zabs_square.
+Hint Resolve Z.abs_nonneg Z.abs_square.
 
 Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
 Proof.
-intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
-assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
-         /\ Zabs p^2 = p^2) by auto.
+intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
+assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
+         /\ Z.abs p^2 = p^2) by auto.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
   (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
@@ -35,7 +35,7 @@ Lemma QnumZpower : forall x : Q, Qnum (x ^ 2)%Q = ((Qnum x) ^ 2) %Z.
 Proof.
   intros.
   destruct x.
-  cbv beta  iota zeta delta - [Zmult].
+  cbv beta  iota zeta delta - [Z.mul].
   ring.
 Qed.
 
@@ -45,15 +45,15 @@ Proof.
   intros.
   destruct x.
   simpl.
-  unfold Zpower_pos.
+  unfold Z.pow_pos.
   simpl.
-  rewrite Pmult_1_r.
+  rewrite Pos.mul_1_r.
   reflexivity.
 Qed.
 
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
- unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r.
+ unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Z.mul_1_r.
  intros HQeq.
  assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 071fb9579..cc8cec470 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -2,26 +2,26 @@
 (* Checks that qualified names are accepted *)
 
 (* New-style syntax *)
-Hint Resolve refl_equal: core arith.
-Hint Immediate trans_equal.
-Hint Unfold sym_equal: core.
+Hint Resolve eq_refl: core arith.
+Hint Immediate eq_trans.
+Hint Unfold eq_sym: core.
 Hint Constructors eq: foo bar.
-Hint Extern 3 (_ = _) => apply refl_equal: foo bar.
+Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
 
 (* Old-style syntax *)
-Hint Resolve refl_equal sym_equal.
-Hint Resolve refl_equal sym_equal: foo.
-Hint Immediate refl_equal sym_equal.
-Hint Immediate refl_equal sym_equal: foo.
-Hint Unfold fst sym_equal.
-Hint Unfold fst sym_equal: foo.
+Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym: foo.
+Hint Immediate eq_refl eq_sym.
+Hint Immediate eq_refl eq_sym: foo.
+Hint Unfold fst eq_sym.
+Hint Unfold fst eq_sym: foo.
 
 (* Checks that local names are accepted *)
 Section A.
   Remark Refl : forall (A : Set) (x : A), x = x.
-  Proof. exact @refl_equal. Defined.
-  Definition Sym := sym_equal.
-  Let Trans := trans_equal.
+  Proof. exact @eq_refl. Defined.
+  Definition Sym := eq_sym.
+  Let Trans := eq_trans.
 
   Hint Resolve Refl: foo.
   Hint Resolve Sym: bar.
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index d43cd0e87..7069bba43 100644
--- a/test-suite/success/MatchFail.v
+++ b/test-suite/success/MatchFail.v
@@ -12,13 +12,13 @@ Ltac compute_POS :=
       let v := constr:X1 in
       match constr:v with
       | 1%positive => fail 1
-      | _ =>  rewrite (BinInt.Zpos_xI v)
+      | _ =>  rewrite (BinInt.Pos2Z.inj_xI v)
       end
   |  |- context [(Zpos (xO ?X1))] =>
       let v := constr:X1 in
       match constr:v with
       | 1%positive => fail 1
-      | _ =>  rewrite (BinInt.Zpos_xO v)
+      | _ =>  rewrite (BinInt.Pos2Z.inj_xO v)
       end
   end.
 
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index f4996734b..17531064c 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -14,38 +14,38 @@ Open Scope Z_scope.
 
 (* zify_op *)
 
-Goal forall a:Z, Zmax a a = a.
+Goal forall a:Z, Z.max a a = a.
 intros.
 omega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b = Zmax b a.
+Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
 omega with *.
 Qed.
 
-Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
 omega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
 omega with *.
 Qed.
 
-Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
 intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
 Qed.
 
-Goal forall a:Z, Zabs a = a -> a >= 0.
+Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
 omega with *.
 Qed.
 
-Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
 omega with *.
 Qed.
@@ -119,7 +119,7 @@ Qed.
 
 (* mix of datatypes *)
 
-Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
 omega with *.
 Qed.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index f8d3ad2c3..28ab33af3 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -22,14 +22,14 @@ Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
 Print merge.
 
 
-Print Zlt.
+Print Z.lt.
 Print Zwf.
 
 Open Local Scope Z_scope.
 
 Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
   match n ?= m with
-    | Lt => Zwfrec n (Zpred m)
+    | Lt => Zwfrec n (Z.pred m)
     | _ => 0
   end.
 
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index bd473fa60..fa659273e 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -14,38 +14,38 @@ Open Scope Z_scope.
 
 (* zify_op *)
 
-Goal forall a:Z, Zmax a a = a.
+Goal forall a:Z, Z.max a a = a.
 intros.
 romega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b = Zmax b a.
+Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
 romega with *.
 Qed.
 
-Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
 romega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
 romega with *.
 Qed.
 
-Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
 intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
 Qed.
 
-Goal forall a:Z, Zabs a = a -> a >= 0.
+Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
 romega with *.
 Qed.
 
-Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
 romega with *.
 Qed.
@@ -119,7 +119,7 @@ Qed.
 
 (* mix of datatypes *)
 
-Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
 romega with *.
 Qed.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 64048fe24..459645f6f 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -378,18 +378,18 @@ Inductive itree : Set :=
 
 Definition isingle l := inode l (fun i => ileaf).
 
-Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
+Definition t1 := inode 0 (fun n => isingle (Z.of_nat (2*n))).
 
 Definition t2 := inode 0
                       (fun n : nat =>
-                               inode (Z_of_nat n)
-                                     (fun p => isingle (Z_of_nat (n*p)))).
+                               inode (Z.of_nat n)
+                                     (fun p => isingle (Z.of_nat (n*p)))).
 
 
 Inductive itree_le : itree-> itree -> Prop :=
   | le_leaf : forall t, itree_le  ileaf t
   | le_node  : forall l l' s s',
-                       Zle l l' ->
+                       Z.le l l' ->
                       (forall i, exists j:nat, itree_le (s i) (s' j)) ->
                       itree_le  (inode  l s) (inode  l' s').
 
@@ -424,7 +424,7 @@ Qed.
 Inductive itree_le' : itree-> itree -> Prop :=
   | le_leaf' : forall t, itree_le'  ileaf t
   | le_node' : forall l l' s s' g,
-                       Zle l l' ->
+                       Z.le l l' ->
                       (forall i, itree_le' (s i) (s' (g i))) ->
                        itree_le'  (inode  l s) (inode  l' s').
 
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 5b37dbd4e..997fedd38 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -3,7 +3,7 @@
 Require Import ZArith.
 
 Module A.
-Definition opp := Zopp.
+Definition opp := Z.opp.
 End A.
 Check (A.opp 3).
 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index d3c761019..0d8bf5560 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -8,8 +8,8 @@ Qed.
 
 Require Import ZArith.
 Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z.
-intros; apply Znot_le_gt, Zgt_lt in H.
-apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
+intros; apply Znot_le_gt, Z.gt_lt in H.
+apply Zmult_lt_reg_r, Z.lt_le_incl in H0; auto.
 Qed.
 
 (* Test application under tuples *)
@@ -266,7 +266,7 @@ Qed.
   (* This works because unfold calls clos_norm_flags which calls nf_evar *)
 
 Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O.
-intros x H; eapply trans_equal;
+intros x H; eapply eq_trans;
 [apply H | unfold x;match goal with |- ?x = ?x => reflexivity end].
 Qed.
 
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
index bc1757fd5..52575eca5 100644
--- a/test-suite/success/decl_mode.v
+++ b/test-suite/success/decl_mode.v
@@ -138,7 +138,7 @@ Coercion IZR: Z >->R.*)
 Open Scope R_scope.
 
 Lemma square_abs_square:
-  forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p).
+  forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p).
 proof.
   assume p:Z.
   per cases on p.
@@ -147,7 +147,7 @@ proof.
     suppose it is (Zpos z).
       thus thesis.
     suppose it is (Zneg z).
-      have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) =
+      have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) =
       (IZR (Zpos z) * IZR (Zpos z))).
            ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))).
       thus ~= (IZR (Zneg z) * IZR (Zneg z)).
@@ -165,15 +165,15 @@ proof.
   have H_in_R:(INR q<>0:>R) by H.
   have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field.
   have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def.
-  have (INR (Zabs_nat p * Zabs_nat p)
-     = (INR (Zabs_nat p) * INR (Zabs_nat p)))
+  have (INR (Z.abs_nat p * Z.abs_nat p)
+     = (INR (Z.abs_nat p) * INR (Z.abs_nat p)))
     by mult_INR.
     ~=  (IZR p* IZR p) by square_abs_square.
     ~=  ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *)
     ~=  ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring.
     ~=  (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0.
     ~= (INR (2%nat * (q*q)))  by sqrt2,mult_INR.
-  then  (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat.
+  then  (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat.
     ~= ((q*q)+(q*q))%nat.
     ~= (Div2.double (q*q)).
   then (q=0%nat) by main_theorem.
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index b25b502cf..23e3caf8a 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -9,12 +9,12 @@ Inductive rBoolOp : Set :=
   | rAnd : rBoolOp
   | rEq : rBoolOp.
 
-Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt.
+Definition rlt (a b : rNat) : Prop := Pos.compare_cont a b Eq = Lt.
 
 Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
 intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
- generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq).
+ generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq).
 intros H' H'0 H'1; right; right; auto.
 intros H' H'0 H'1; left; unfold rlt in |- *.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
index d9ade3144..9edfd8255 100644
--- a/test-suite/success/searchabout.v
+++ b/test-suite/success/searchabout.v
@@ -55,6 +55,6 @@ SearchAbout [-"*"%nat "+"%nat] outside Logic.
 
 Require Import ZArith.
 
-SearchAbout Zmult Zplus "distr".
+SearchAbout Z.mul Z.add "distr".
 SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
 SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 578373217..c5f032beb 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -5,20 +5,20 @@ intros.
 (* "compatibility" mode: specializing a global name
    means a kind of generalize *)
 
-specialize trans_equal. intros _.
-specialize trans_equal with (1:=H)(2:=H0). intros _.
-specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _.
-specialize trans_equal with (1:=H)(z:=c). intros _.
-specialize trans_equal with nat a b c. intros _.
-specialize (@trans_equal nat). intros _.
-specialize (@trans_equal _ a b c). intros _.
-specialize (trans_equal (x:=a)). intros _.
-specialize (trans_equal (x:=a)(y:=b)). intros _.
-specialize (trans_equal H H0). intros _.
-specialize (trans_equal H0 (z:=b)). intros _.
+specialize eq_trans. intros _.
+specialize eq_trans with (1:=H)(2:=H0). intros _.
+specialize eq_trans with (x:=a)(y:=b)(z:=c). intros _.
+specialize eq_trans with (1:=H)(z:=c). intros _.
+specialize eq_trans with nat a b c. intros _.
+specialize (@eq_trans nat). intros _.
+specialize (@eq_trans _ a b c). intros _.
+specialize (eq_trans (x:=a)). intros _.
+specialize (eq_trans (x:=a)(y:=b)). intros _.
+specialize (eq_trans H H0). intros _.
+specialize (eq_trans H0 (z:=b)). intros _.
 
 (* local "in place" specialization *)
-assert (Eq:=trans_equal).
+assert (Eq:=eq_trans).
 
 specialize Eq.
 specialize Eq with (1:=H)(2:=H0). Undo.
@@ -38,10 +38,10 @@ specialize (Eq _ _ _ b H0). Undo.
     presque ok... *)
 
 (* 2) echoue moins lorsque zero premise de mangé *)
-specialize trans_equal with (1:=Eq).  (* mal typé !! *)
+specialize eq_trans with (1:=Eq).  (* mal typé !! *)
 
 (* 3) *)
-specialize trans_equal with _ a b c. intros _.
+specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)
 
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index 8b7764e5c..42e32cccc 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -75,7 +75,7 @@ Notation "x ≤ y" := (x<=y) (at level 70, no associativity).
 
 Require Import ZArith.
 Open Scope Z_scope.
-Locate "≤". (* still le, not Zle *)
+Locate "≤". (* still le, not Z.le *)
 Notation "x ≤ y" := (x<=y) (at level 70, no associativity).
 Locate "≤".
 Close Scope Z_scope.