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

12 files changed, 43 insertions, 43 deletions

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}.