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

16 files changed, 79 insertions, 79 deletions

diff --git a/doc/RecTutorial/RecTutorial.tex b/doc/RecTutorial/RecTutorial.tex
index f2cb383e04..857ba84d77 100644
--- a/doc/RecTutorial/RecTutorial.tex
+++ b/doc/RecTutorial/RecTutorial.tex
@@ -560,11 +560,11 @@ as it can be infered from $a$.
 \begin{alltt}
 Print eq.
 \it{} Inductive eq (A : Type) (x : A) : A \arrow{} Prop :=  
-    refl_equal : x = x
+    eq_refl : x = x
 For eq: Argument A is implicit
-For refl_equal: Argument A is implicit
+For eq_refl: Argument A is implicit
 For eq: Argument scopes are [type_scope _ _]
-For refl_equal: Argument scopes are [type_scope _]
+For eq_refl: Argument scopes are [type_scope _]
 \end{alltt}
 
 Notice also that  the first parameter $A$ of \texttt{eq} has type
@@ -581,15 +581,15 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Lemma eq_proof_proof : eq_refl (2*6) = eq_refl (3*4).
 Proof.
  reflexivity.
 Qed.
 
 Print eq_proof_proof.
 \it eq_proof_proof = 
-refl_equal (refl_equal (3 * 4))
-     : refl_equal (2 * 6) = refl_equal (3 * 4)
+eq_refl (eq_refl (3 * 4))
+     : eq_refl (2 * 6) = eq_refl (3 * 4)
 \tt
 
 Lemma eq_lt_le : ( 2 < 4) = (3 {\coqle} 4).
@@ -942,10 +942,10 @@ predecessor =  fun n : nat {\funarrow}
 \textbf{| O {\funarrow}}
     exist (fun m : nat {\funarrow} 0 = 0 {\coqand} m = 0 {\coqor} 0 = S m) 0
       (or_introl (0 = 1) 
-                 (conj (refl_equal 0) (refl_equal 0)))
+                 (conj (eq_refl 0) (eq_refl 0)))
 \textbf{| S n0 {\funarrow}}
     exist (fun m : nat {\funarrow} S n0 = 0 {\coqand} m = 0 {\coqor} S n0 = S m) n0
-      (or_intror (S n0 = 0 {\coqand} n0 = 0) (refl_equal (S n0)))
+      (or_intror (S n0 = 0 {\coqand} n0 = 0) (eq_refl (S n0)))
 \textbf{end}  : {\prodsym} n : nat, \textbf{pred_spec n}
 \end{alltt}
 
@@ -1084,7 +1084,7 @@ The following term is a proof  of ``~$Q\;a\, \arrow{}\, Q\;b$~''.
 \begin{alltt}
 fun H : Q a {\funarrow}
   match \(\pi\) in (_ = y) return Q y with
-     refl_equal {\funarrow} H
+     eq_refl {\funarrow} H
   end
 \end{alltt}
 Notice the header of the \texttt{match} construct.
@@ -1552,13 +1552,13 @@ node, a tree of height 1 and a tree of height 2:
 \begin{alltt}
 Definition isingle l := inode l (fun i {\funarrow} ileaf).
 
-Definition t1 := inode 0 (fun n {\funarrow} isingle (Z_of_nat n)).
+Definition t1 := inode 0 (fun n {\funarrow} isingle (Z.of_nat n)).
 
 Definition t2 := 
  inode 0 
       (fun n : nat {\funarrow} 
-                   inode (Z_of_nat n)
-                   (fun p {\funarrow} isingle (Z_of_nat (n*p)))).
+                   inode (Z.of_nat n)
+                   (fun p {\funarrow} isingle (Z.of_nat (n*p)))).
 \end{alltt}
 
 
@@ -1572,7 +1572,7 @@ appear:
 Inductive itree_le : itree{\arrow} itree {\arrow} Prop :=
   | le_leaf : {\prodsym} t, itree_le  ileaf t
   | le_node : {\prodsym} l l' s s', 
-                Zle l l' {\arrow} 
+                Z.le l l' {\arrow}
                 ({\prodsym} i, {\exsym} j:nat, itree_le (s i) (s' j)){\arrow} 
                 itree_le  (inode  l s) (inode  l' s').
 
@@ -1597,7 +1597,7 @@ the type of \texttt{itree\_le}, does not present this problem:
 Inductive itree_le' : itree{\arrow} itree {\arrow} Prop :=
   | le_leaf'  : {\prodsym} t, itree_le'  ileaf t
   | le_node' : {\prodsym} l l' s s' g, 
-                  Zle l l' {\arrow}  
+                  Z.le l l' {\arrow}
                   ({\prodsym} i, itree_le' (s i) (s' (g i))) {\arrow} 
                   itree_le'  (inode  l s) (inode  l' s').
 
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
index 28aaf75204..8cfeebc28b 100644
--- a/doc/RecTutorial/RecTutorial.v
+++ b/doc/RecTutorial/RecTutorial.v
@@ -83,7 +83,7 @@ Proof.
 Qed.
 Print eq_3_3.
 
-Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Lemma eq_proof_proof : eq_refl (2*6) = eq_refl (3*4).
 Proof.
  reflexivity.
 Qed.
@@ -241,7 +241,7 @@ Section equality_elimination.
            (Q : A -> Type).
  Check (fun H : Q a =>
   match p in (eq _  y) return Q y with
-     refl_equal => H
+     eq_refl => H
   end).
 
 End equality_elimination.
@@ -377,18 +377,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').
 
@@ -423,7 +423,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/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index b63f3ee26c..5ce5e0436c 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -545,7 +545,7 @@ dependent elimination of reflexive equality proofs.
 \begin{coq_example*}
 Axiom Streicher_K :
   forall (A:Type) (x:A) (P: x=x -> Prop),
-    P (refl_equal x) -> forall p: x=x, P p.
+    P (eq_refl x) -> forall p: x=x, P p.
 \end{coq_example*}
 
 In the general case, axiom $K$ is an independent statement of the
@@ -563,7 +563,7 @@ Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2.
 Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98}
 
 \begin{coq_example*}
-Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x.
+Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = eq_refl x.
 \end{coq_example*}
 
 Axiom $K$ is also equivalent to 
@@ -2108,7 +2108,7 @@ Yes, because equality is decidable on {\tt nat}. Here is the proof.
 Require Import Eqdep_dec.
 Require Import Peano_dec.
 Theorem K_nat :
-  forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
+  forall (x:nat) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
 Proof.
 intros; apply K_dec_set with (p := p).
 apply eq_nat_dec.
@@ -2139,16 +2139,16 @@ Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
 Proof.
 induction p using le_ind'; intro q.
  replace (le_n n) with
-  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ eq_refl).
  2:reflexivity.
-  generalize (refl_equal n).
+  generalize (eq_refl n).
     pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
      rewrite <- eq_rect_eq_nat; trivial.
      contradiction (le_Sn_n m); rewrite <- e; assumption.
  replace (le_S n m p) with
-  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ eq_refl).
  2:reflexivity.
-  generalize (refl_equal (S m)).
+  generalize (eq_refl (S m)).
     pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
      contradiction (le_Sn_n m); rewrite Heq; assumption.
      injection HeqS; intro Heq; generalize l HeqS.
@@ -2536,7 +2536,7 @@ existential variables.
 Lemma example_show_existentials :  forall a b c:nat, a=b -> b=c -> a=c.
 Proof.
 intros.
-eapply trans_equal.
+eapply eq_trans.
 Show Existentials.
 eassumption.
 assumption.
diff --git a/doc/faq/interval_discr.v b/doc/faq/interval_discr.v
index ed2c0e37ee..671dc988a2 100644
--- a/doc/faq/interval_discr.v
+++ b/doc/faq/interval_discr.v
@@ -32,16 +32,16 @@ Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
 Proof.
 induction p using le_ind'; intro q.
  replace (le_n n) with
-  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
+  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ eq_refl).
  2:reflexivity.
-  generalize (refl_equal n).
+  generalize (eq_refl n).
     pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
      rewrite <- eq_rect_eq_nat; trivial.
      contradiction (le_Sn_n m); rewrite <- e; assumption.
  replace (le_S n m p) with
-  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
+  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ eq_refl).
  2:reflexivity.
-  generalize (refl_equal (S m)).
+  generalize (eq_refl (S m)).
     pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
      contradiction (le_Sn_n m); rewrite Heq; assumption.
      injection HeqS; intro Heq; generalize l HeqS.
@@ -216,7 +216,7 @@ Lemma inj_restrict :
 Proof.
 intros A f x y z Hfinj Hneqx Hfy Hfx Heq.
 assert (f z <> f x).
-  apply sym_not_eq.
+  apply not_eq_sym.
   intro Heqf.
   apply Hneqx.
   apply Hfinj.
@@ -292,7 +292,7 @@ destruct (le_lt_dec (f xSn) (f y)) as [Hlefy|Hgefy].
 assert (Heq : x = y).
   apply Hfinj.
   assert (f xSn <> f y).
-    apply sym_not_eq.
+    apply not_eq_sym.
     intro Heqf.
     apply Hneqy.
     apply Hfinj.
@@ -302,7 +302,7 @@ assert (Heq : x = y).
     apply le_O_n.
     apply le_neq_lt; assumption.
   assert (f xSn <> f x).
-    apply sym_not_eq.
+    apply not_eq_sym.
     intro Heqf.
     apply Hneqx.
     apply Hfinj.
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 20ff649aac..f7c4bd5caf 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -71,7 +71,7 @@ Leibniz equality on some type. An example implementation is:
 Instance unit_EqDec : EqDec unit :=
 { eqb x y := true ;
   eqb_leibniz x y H := 
-    match x, y return x = y with tt, tt => refl_equal tt end }.
+    match x, y return x = y with tt, tt => eq_refl tt end }.
 \end{coq_example*}
 
 If one does not give all the members in the \texttt{Instance}
diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex
index 9a9abe5dff..f33c0d3563 100644
--- a/doc/refman/Natural.tex
+++ b/doc/refman/Natural.tex
@@ -158,7 +158,7 @@ Add Natural Implicit constr1.
 By default, the proposition (or predicate) constructors
 
 \verb=conj=, \verb=or_introl=, \verb=or_intror=, \verb=ex_intro=,
-\verb=exT_intro=, \verb=refl_equal=, \verb=refl_eqT= and \verb=exist=
+\verb=eq_refl= and \verb=exist=
 
 \noindent are declared implicit. Note that declaring implicit the
 constructor of a datatype (i.e. an inductive type of type \verb=Set=)
diff --git a/doc/refman/Omega.tex b/doc/refman/Omega.tex
index b9e899ce89..213c050615 100644
--- a/doc/refman/Omega.tex
+++ b/doc/refman/Omega.tex
@@ -51,7 +51,7 @@ on atomic formulas. Atomic formulas are built from the predicates
 and in expressions of type \verb=Z=, {\tt omega} recognizes 
 
 \begin{quote}
-\verb!+, -, *, Zsucc!, and constants.
+\verb!+, -, *, Z.succ!, and constants.
 \end{quote}
 
 All expressions of type \verb=nat= or \verb=Z= not built on these
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
index 3898bf4c4b..664c0d3ff2 100644
--- a/doc/refman/Polynom.tex
+++ b/doc/refman/Polynom.tex
@@ -927,7 +927,7 @@ Open Scope Z_scope.
 Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
 \end{coq_example}
 \begin{coq_example*}
-intros; rewrite (Zmult_comm y z); reflexivity.
+intros; rewrite (Z.mul_comm y z); reflexivity.
 Save toto.
 \end{coq_example*}
 \begin{coq_example}
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 96073d71a6..fee070fd65 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -53,7 +53,7 @@ will be first rewrote to:
   (match x as y return (x = y -> _) with
   | 0 => fun H : x = 0 -> t
   | S n => fun H : x = S n -> u
-  end) (refl_equal n).
+  end) (eq_refl n).
 \end{coq_example*}
   
   This permits to get the proper equalities in the context of proof
diff --git a/doc/refman/RefMan-coi.tex b/doc/refman/RefMan-coi.tex
index e609fce825..d75b9eb93c 100644
--- a/doc/refman/RefMan-coi.tex
+++ b/doc/refman/RefMan-coi.tex
@@ -277,7 +277,7 @@ an infinite object of type
 definition.
 \begin{coq_example}
 CoFixpoint eqproof (s1 s2:Stream A) : EqSt s1 (conc s1 s2) :=
-  eqst s1 (conc s1 s2) (refl_equal (hd A (conc s1 s2)))
+  eqst s1 (conc s1 s2) (eq_refl (hd A (conc s1 s2)))
     (eqproof (tl A s1) s2).
 \end{coq_example}
 \begin{coq_eval}
diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index a9feb34c5a..6fa7596dbc 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -566,16 +566,16 @@ clause where {\ident} is dependent in the return type.
 For instance, in the following example:
 \begin{coq_example*}
 Inductive bool : Type := true : bool | false : bool.
-Inductive eq (A:Type) (x:A) : A -> Prop := refl_equal : eq A x x.
+Inductive eq (A:Type) (x:A) : A -> Prop := eq_refl : eq A x x.
 Inductive or (A:Prop) (B:Prop) : Prop :=
 | or_introl : A -> or A B
 | or_intror : B -> or A B.
 Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
 := match b as x return or (eq bool x true) (eq bool x false) with
    | true  => or_introl (eq bool true true) (eq bool true false)
-                (refl_equal bool true)
+                (eq_refl bool true)
    | false => or_intror (eq bool false true) (eq bool false false)
-                (refl_equal bool false)
+                (eq_refl bool false)
    end.
 \end{coq_example*}
 the branches have respective types {\tt or (eq bool true true) (eq
@@ -591,9 +591,9 @@ same meaning as the previous one.
 Definition bool_case (b:bool) : or (eq bool b true) (eq bool b false)
 := match b return or (eq bool b true) (eq bool b false) with
    | true  => or_introl (eq bool true true) (eq bool true false)
-                (refl_equal bool true)
+                (eq_refl bool true)
    | false => or_intror (eq bool false true) (eq bool false false)
-                (refl_equal bool false)
+                (eq_refl bool false)
    end.
 \end{coq_example*}
 
@@ -621,9 +621,9 @@ the return type is not dependent on them.
 
 For instance, in the following example:
 \begin{coq_example*}
-Definition sym_equal (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
+Definition eq_sym (A:Type) (x y:A) (H:eq A x y) : eq A y x :=
   match H in eq _ _ z return eq A z x with
-  | refl_equal => refl_equal A x
+  | eq_refl => eq_refl A x
   end.
 \end{coq_example*}
 the type of the branch has type {\tt eq~A~x~x} because the third
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex
index 31c6fef4a1..26c564e52f 100644
--- a/doc/refman/RefMan-lib.tex
+++ b/doc/refman/RefMan-lib.tex
@@ -220,11 +220,11 @@ define \verb:eq: as the smallest reflexive relation, and it is also
 equivalent to Leibniz' equality.
 
 \ttindex{eq}
-\ttindex{refl\_equal}
+\ttindex{eq\_refl}
 
 \begin{coq_example*}
 Inductive eq (A:Type) (x:A) : A -> Prop :=
-    refl_equal : eq A x x.
+    eq_refl : eq A x x.
 \end{coq_example*}
 
 \subsubsection[Lemmas]{Lemmas\label{PreludeLemmas}}
@@ -239,8 +239,8 @@ Theorem absurd : forall A C:Prop, A -> ~ A -> C.
 \begin{coq_eval}
 Abort.
 \end{coq_eval}
-\ttindex{sym\_eq}
-\ttindex{trans\_eq}
+\ttindex{eq\_sym}
+\ttindex{eq\_trans}
 \ttindex{f\_equal}
 \ttindex{sym\_not\_eq}
 \begin{coq_example*}
@@ -248,10 +248,10 @@ Section equality.
 Variables A B : Type.
 Variable f : A -> B.
 Variables x y z : A.
-Theorem sym_eq : x = y -> y = x.
-Theorem trans_eq : x = y -> y = z -> x = z.
+Theorem eq_sym : x = y -> y = x.
+Theorem eq_trans : x = y -> y = z -> x = z.
 Theorem f_equal : x = y -> f x = f y.
-Theorem sym_not_eq : x <> y -> y <> x.
+Theorem not_eq_sym : x <> y -> y <> x.
 \end{coq_example*}
 \begin{coq_eval}
 Abort.
@@ -280,7 +280,7 @@ Abort.
 \end{coq_eval}
 %Abort (for now predefined eq_rect)
 \begin{coq_example*}
-Hint Immediate sym_eq sym_not_eq : core.
+Hint Immediate eq_sym not_eq_sym : core.
 \end{coq_example*}
 \ttindex{f\_equal$i$}
 
@@ -864,22 +864,22 @@ module {\tt ZArith} and opening scope {\tt Z\_scope}.
 \begin{tabular}{l|l|l|l}
 Notation & Interpretation & Precedence & Associativity\\
 \hline
-\verb!_ < _! & {\tt Zlt} &&\\
-\verb!x <= y! & {\tt Zle} &&\\
-\verb!_ > _! & {\tt Zgt} &&\\
-\verb!x >= y! & {\tt Zge} &&\\
+\verb!_ < _! & {\tt Z.lt} &&\\
+\verb!x <= y! & {\tt Z.le} &&\\
+\verb!_ > _! & {\tt Z.gt} &&\\
+\verb!x >= y! & {\tt Z.ge} &&\\
 \verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
 \verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
 \verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
 \verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
-\verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
-\verb!_ + _! & {\tt Zplus} &&\\
-\verb!_ - _! & {\tt Zminus} &&\\
-\verb!_ * _! & {\tt Zmult} &&\\
-\verb!_ / _! & {\tt Zdiv} &&\\
-\verb!_ mod _! & {\tt Zmod} & 40 & no \\
-\verb!- _!  & {\tt Zopp} &&\\
-\verb!_ ^ _! & {\tt Zpower} &&\\
+\verb!_ ?= _! & {\tt Z.compare} & 70 & no\\
+\verb!_ + _! & {\tt Z.add} &&\\
+\verb!_ - _! & {\tt Z.sub} &&\\
+\verb!_ * _! & {\tt Z.mul} &&\\
+\verb!_ / _! & {\tt Z.div} &&\\
+\verb!_ mod _! & {\tt Z.modulo} & 40 & no \\
+\verb!- _!  & {\tt Z.opp} &&\\
+\verb!_ ^ _! & {\tt Z.pow} &&\\
 \end{tabular}
 \end{center}
 \caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index d7f00584e0..f10b9c3ee5 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -607,7 +607,7 @@ Ltac f x :=
   match x with
     context f [S ?X] => 
     idtac X;                    (* To display the evaluation order *)
-    assert (p := refl_equal 1 : X=1);    (* To filter the case X=1 *)
+    assert (p := eq_refl 1 : X=1);    (* To filter the case X=1 *)
     let x:= context f[O] in assert (x=O) (* To observe the context *)
   end.
 Goal True.
@@ -1205,7 +1205,7 @@ Axiom AR_unit : (A -> unit) = unit.
 Axiom AL_unit : (unit -> A) = A.
 Lemma Cons : B = C -> A * B = A * C.
 Proof.
-intro Heq; rewrite Heq; apply refl_equal.
+intro Heq; rewrite Heq; reflexivity.
 Qed.
 End Iso_axioms.
 \end{coq_example*}
@@ -1272,7 +1272,7 @@ Ltac assoc := repeat rewrite <- Ass.
 \begin{coq_example}
 Ltac DoCompare n :=
   match goal with
-  | [ |- (?A = ?A) ] => apply refl_equal
+  | [ |- (?A = ?A) ] => reflexivity
   | [ |- (?A * ?B = ?A * ?C) ] =>
     apply Cons; let newn := Length B in DoCompare newn
   | [ |- (?A * ?B = ?C) ] =>
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index f81811430d..4208787fcc 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -266,7 +266,7 @@ may be enclosed by optional {\tt [  ]} delimiters.
 Require Import ZArith.
 \end{coq_example*}
 \begin{coq_example}
-SearchAbout Zmult Zplus "distr".
+SearchAbout Z.mul Z.add "distr".
 SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
 SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
 \end{coq_example}
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex
index 8330a434bd..91ff3d5ece 100644
--- a/doc/refman/RefMan-tacex.tex
+++ b/doc/refman/RefMan-tacex.tex
@@ -1129,7 +1129,7 @@ red; intros (x, (y, Hy)).
 elim (Hy 0); elim (Hy 1); elim (Hy 2); intros;
  match goal with
  | [_:(?a = ?b),_:(?a = ?c) |- _ ] =>
-     cut (b = c); [ discriminate | apply trans_equal with a; auto ]
+     cut (b = c); [ discriminate | transitivity a; auto ]
  end.
 Qed.
 \end{coq_example*}
@@ -1379,7 +1379,7 @@ Axiom AR_unit : (A -> unit) = unit.
 Axiom AL_unit : (unit -> A) = A.
 Lemma Cons : B = C -> A * B = A * C.
 Proof.
-intro Heq; rewrite Heq; apply refl_equal.
+intro Heq; rewrite Heq; reflexivity.
 Qed.
 End Iso_axioms.
 \end{coq_example*}
@@ -1439,7 +1439,7 @@ Ltac assoc := repeat rewrite <- Ass.
 \begin{coq_example}
 Ltac DoCompare n :=
   match goal with
-  | [ |- (?A = ?A) ] => apply refl_equal
+  | [ |- (?A = ?A) ] => reflexivity
   | [ |- (?A * ?B = ?A * ?C) ] =>
       apply Cons; let newn := Length B in
                   DoCompare newn
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index 8e1bb10c9b..c0913135c9 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -371,9 +371,9 @@ the replaced term occurs in a covariant position.
 
 \begin{cscexample}[Covariance and contravariance]
 Suppose that division over real numbers has been defined as a
-morphism of signature \texttt{Zdiv: Zlt ++> Zlt -{}-> Zlt} (i.e.
-\texttt{Zdiv} is increasing in its first argument, but decreasing on the
-second one). Let \texttt{<} denotes \texttt{Zlt}. 
+morphism of signature \texttt{Z.div: Z.lt ++> Z.lt -{}-> Z.lt} (i.e.
+\texttt{Z.div} is increasing in its first argument, but decreasing on the
+second one). Let \texttt{<} denotes \texttt{Z.lt}.
 Under the hypothesis \texttt{H: x < y} we have
 \texttt{k < x / y -> k < x / x}, but not
 \texttt{k < y / x -> k < x / x}.