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

2 files changed, 15 insertions, 15 deletions

diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index b63f3ee26..5ce5e0436 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 ed2c0e37e..671dc988a 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.