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, 15 insertions, 15 deletions

diff --git a/theories/ZArith/Zdigits.v b/theories/ZArith/Zdigits.v
index ff1d96df4..a9348785a 100644
--- a/theories/ZArith/Zdigits.v
+++ b/theories/ZArith/Zdigits.v
@@ -64,7 +64,7 @@ Section ENCODING_VALUE.
 
 (** We compute the binary value via a Horner scheme.
     Computation stops at the vector length without checks.
-    We define a function Zmod2 similar to Zdiv2 returning the
+    We define a function Zmod2 similar to Z.div2 returning the
     quotient of division z=2q+r with 0<=r<=1.
     The two's complement value is also computed via a Horner scheme
     with Zmod2, the parameter is the size minus one.
@@ -88,7 +88,7 @@ Section ENCODING_VALUE.
 
 
   Lemma Zmod2_twice :
-    forall z:Z, z = (2 * Zmod2 z + bit_value (Zeven.Zodd_bool z))%Z.
+    forall z:Z, z = (2 * Zmod2 z + bit_value (Z.odd z))%Z.
   Proof.
     destruct z; simpl in |- *.
     trivial.
@@ -97,7 +97,7 @@ Section ENCODING_VALUE.
 
     destruct p; simpl in |- *.
     destruct p as [p| p| ]; simpl in |- *.
-    rewrite <- (Pdouble_minus_one_o_succ_eq_xI p); trivial.
+    rewrite <- (Pos.pred_double_succ p); trivial.
 
     trivial.
 
@@ -113,15 +113,15 @@ Section ENCODING_VALUE.
     simple induction n; intros.
     exact Bnil.
 
-    exact (Bcons (Zeven.Zodd_bool H0) n0 (H (Zeven.Zdiv2 H0))).
+    exact (Bcons (Z.odd H0) n0 (H (Z.div2 H0))).
   Defined.
 
   Lemma Z_to_two_compl : forall n:nat, Z -> Bvector (S n).
   Proof.
     simple induction n; intros.
-    exact (Bcons (Zeven.Zodd_bool H) 0 Bnil).
+    exact (Bcons (Z.odd H) 0 Bnil).
 
-    exact (Bcons (Zeven.Zodd_bool H0) (S n0) (H (Zmod2 H0))).
+    exact (Bcons (Z.odd H0) (S n0) (H (Zmod2 H0))).
   Defined.
 
 End ENCODING_VALUE.
@@ -175,27 +175,27 @@ Section Z_BRIC_A_BRAC.
     destruct b; destruct z as [| p| p]; auto.
     destruct p as [p| p| ]; auto.
     destruct p as [p| p| ]; simpl in |- *; auto.
-    intros; rewrite (Psucc_o_double_minus_one_eq_xO p); trivial.
+    intros; rewrite (Pos.succ_pred_double p); trivial.
   Qed.
 
   Lemma Z_to_binary_Sn_z :
     forall (n:nat) (z:Z),
       Z_to_binary (S n) z =
-      Bcons (Zeven.Zodd_bool z) n (Z_to_binary n (Zeven.Zdiv2 z)).
+      Bcons (Z.odd z) n (Z_to_binary n (Z.div2 z)).
   Proof.
     intros; auto.
   Qed.
 
   Lemma Z_div2_value :
     forall z:Z,
-      (z >= 0)%Z -> (bit_value (Zeven.Zodd_bool z) + 2 * Zeven.Zdiv2 z)%Z = z.
+      (z >= 0)%Z -> (bit_value (Z.odd z) + 2 * Z.div2 z)%Z = z.
   Proof.
     destruct z as [| p| p]; auto.
     destruct p; auto.
     intro H; elim H; trivial.
   Qed.
 
-  Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Zeven.Zdiv2 z >= 0)%Z.
+  Lemma Pdiv2 : forall z:Z, (z >= 0)%Z -> (Z.div2 z >= 0)%Z.
   Proof.
     destruct z as [| p| p].
     auto.
@@ -209,10 +209,10 @@ Section Z_BRIC_A_BRAC.
   Lemma Zdiv2_two_power_nat :
     forall (z:Z) (n:nat),
       (z >= 0)%Z ->
-      (z < two_power_nat (S n))%Z -> (Zeven.Zdiv2 z < two_power_nat n)%Z.
+      (z < two_power_nat (S n))%Z -> (Z.div2 z < two_power_nat n)%Z.
   Proof.
     intros.
-    cut (2 * Zeven.Zdiv2 z < 2 * two_power_nat n)%Z; intros.
+    cut (2 * Z.div2 z < 2 * two_power_nat n)%Z; intros.
     omega.
 
     rewrite <- two_power_nat_S.
@@ -225,13 +225,13 @@ Section Z_BRIC_A_BRAC.
   Lemma Z_to_two_compl_Sn_z :
     forall (n:nat) (z:Z),
       Z_to_two_compl (S n) z =
-      Bcons (Zeven.Zodd_bool z) (S n) (Z_to_two_compl n (Zmod2 z)).
+      Bcons (Z.odd z) (S n) (Z_to_two_compl n (Zmod2 z)).
   Proof.
     intros; auto.
   Qed.
 
   Lemma Zeven_bit_value :
-    forall z:Z, Zeven.Zeven z -> bit_value (Zeven.Zodd_bool z) = 0%Z.
+    forall z:Z, Zeven.Zeven z -> bit_value (Z.odd z) = 0%Z.
   Proof.
     destruct z; unfold bit_value in |- *; auto.
     destruct p; tauto || (intro H; elim H).
@@ -239,7 +239,7 @@ Section Z_BRIC_A_BRAC.
   Qed.
 
   Lemma Zodd_bit_value :
-    forall z:Z, Zeven.Zodd z -> bit_value (Zeven.Zodd_bool z) = 1%Z.
+    forall z:Z, Zeven.Zodd z -> bit_value (Z.odd z) = 1%Z.
   Proof.
     destruct z; unfold bit_value in |- *; auto.
     intros; elim H.