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

13 files changed, 65 insertions, 65 deletions

diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 071fb9579e..cc8cec4707 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 d43cd0e874..7069bba430 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 f4996734bf..17531064cc 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 f8d3ad2c35..28ab33af30 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 bd473fa607..fa659273e1 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 64048fe24e..459645f6f8 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 5b37dbd4e1..997fedd38f 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 d3c7610193..0d8bf5560c 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 bc1757fd53..52575eca5f 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 b25b502cf4..23e3caf8a3 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 d9ade3144b..9edfd82556 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 5783732174..c5f032beb0 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 8b7764e5cc..42e32ccccb 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.