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

1 files changed, 7 insertions, 7 deletions

diff --git a/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index 2bf3d8c35..b43ce6f04 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -109,7 +109,7 @@ Qed.
 
 Lemma Zring_morph :
   ring_morph 0 1 rplus rtimes rminus ropp req
-             0%Z 1%Z Zplus Zmult Zminus Zopp
+             0%Z 1%Z Z.add Z.mul Z.sub Z.opp
              Zeq_bool gen_order_phi_Z.
 Proof.
 exact (gen_phiZ_morph sor.(SORsetoid) ring_ops_wd sor.(SORrt)).
@@ -122,7 +122,7 @@ try apply (Rplus_pos_pos sor); try apply (Rtimes_pos_pos sor); try apply (Rplus_
 try apply (Rlt_0_1 sor); assumption.
 Qed.
 
-Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Psucc x) == 1 + phi_pos1 x.
+Lemma phi_pos1_succ : forall x : positive, phi_pos1 (Pos.succ x) == 1 + phi_pos1 x.
 Proof.
 exact (ARgen_phiPOS_Psucc sor.(SORsetoid) ring_ops_wd
         (Rth_ARth sor.(SORsetoid) ring_ops_wd sor.(SORrt))).
@@ -130,7 +130,7 @@ Qed.
 
 Lemma clt_pos_morph : forall x y : positive, (x < y)%positive -> phi_pos1 x < phi_pos1 y.
 Proof.
-intros x y H. pattern y; apply Plt_ind with x.
+intros x y H. pattern y; apply Pos.lt_ind with x.
 rewrite phi_pos1_succ; apply (Rlt_succ_r sor).
 clear y H; intros y _ H. rewrite phi_pos1_succ. now apply (Rlt_lt_succ sor).
 assumption.
@@ -150,9 +150,9 @@ apply -> (Ropp_lt_mono sor); apply clt_pos_morph.
 red. now rewrite Pos.compare_antisym.
 Qed.
 
-Lemma Zcleb_morph : forall x y : Z, Zle_bool x y = true -> [x] <= [y].
+Lemma Zcleb_morph : forall x y : Z, Z.leb x y = true -> [x] <= [y].
 Proof.
-unfold Zle_bool; intros x y H.
+unfold Z.leb; intros x y H.
 case_eq (x ?= y)%Z; intro H1; rewrite H1 in H.
 le_equal. apply Zring_morph.(morph_eq). unfold Zeq_bool; now rewrite H1.
 le_less. now apply clt_morph.
@@ -162,9 +162,9 @@ Qed.
 Lemma Zcneqb_morph : forall x y : Z, Zeq_bool x y = false -> [x] ~= [y].
 Proof.
 intros x y H. unfold Zeq_bool in H.
-case_eq (Zcompare x y); intro H1; rewrite H1 in *; (discriminate || clear H).
+case_eq (Z.compare x y); intro H1; rewrite H1 in *; (discriminate || clear H).
 apply (Rlt_neq sor). now apply clt_morph.
-fold (x > y)%Z in H1. rewrite Zgt_iff_lt in H1.
+fold (x > y)%Z in H1. rewrite Z.gt_lt_iff in H1.
 apply (Rneq_symm sor). apply (Rlt_neq sor). now apply clt_morph.
 Qed.