Deletion of useless Zdigits_def

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 23 insertions, 23 deletions

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index cb16e1291..0142b36be 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -678,17 +678,17 @@ Module Make (N:NType) <: ZType.
   destruct (norm_pos x) as [x'|x'];
    specialize (H x' (eq_refl _)) || clear H.
 
- Lemma spec_testbit: forall x p, testbit x p = Ztestbit (to_Z x) (to_Z p).
+ Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p).
  Proof.
   intros x p. unfold testbit.
   destr_norm_pos p; simpl. destr_norm_pos x; simpl.
   apply N.spec_testbit.
   rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith.
   symmetry. apply Z.bits_opp. apply N.spec_pos.
-  symmetry. apply Ztestbit_neg_r; auto with zarith.
+  symmetry. apply Z.testbit_neg_r; auto with zarith.
  Qed.
 
- Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Zshiftl (to_Z x) (to_Z p).
+ Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p).
  Proof.
   intros x p. unfold shiftl.
   destr_norm_pos x; destruct p as [p|p]; simpl;
@@ -703,13 +703,13 @@ Module Make (N:NType) <: ZType.
   now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2.
  Qed.
 
- Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Zshiftr (to_Z x) (to_Z p).
+ Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p).
  Proof.
   intros. unfold shiftr. rewrite spec_shiftl, spec_opp.
   apply Z.shiftl_opp_r.
  Qed.
 
- Lemma spec_land: forall x y, to_Z (land x y) = Zand (to_Z x) (to_Z y).
+ Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold land.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -720,7 +720,7 @@ Module Make (N:NType) <: ZType.
   now rewrite Z.lnot_lor, !Zlnot_alt2.
  Qed.
 
- Lemma spec_lor: forall x y, to_Z (lor x y) = Zor (to_Z x) (to_Z y).
+ Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold lor.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -731,7 +731,7 @@ Module Make (N:NType) <: ZType.
   now rewrite Z.lnot_land, !Zlnot_alt2.
  Qed.
 
- Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Zdiff (to_Z x) (to_Z y).
+ Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold ldiff.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -742,7 +742,7 @@ Module Make (N:NType) <: ZType.
   now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3.
  Qed.
 
- Lemma spec_lxor: forall x y, to_Z (lxor x y) = Zxor (to_Z x) (to_Z y).
+ Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y).
  Proof.
   intros x y. unfold lxor.
   destr_norm_pos x; destr_norm_pos y; simpl;
@@ -753,9 +753,9 @@ Module Make (N:NType) <: ZType.
   now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2.
  Qed.
 
- Lemma spec_div2: forall x, to_Z (div2 x) = Zdiv2 (to_Z x).
+ Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x).
  Proof.
-  intros x. unfold div2. now rewrite spec_shiftr, Zdiv2_spec, spec_1.
+  intros x. unfold div2. now rewrite spec_shiftr, Z.div2_spec, spec_1.
  Qed.
 
 End Make.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index f40928566..eaab13c2a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -445,77 +445,77 @@ Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
 
 Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true.
 Proof.
- intros. zify. apply Ztestbit_odd_0.
+ intros. zify. apply Z.testbit_odd_0.
 Qed.
 
 Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false.
 Proof.
- intros. zify. apply Ztestbit_even_0.
+ intros. zify. apply Z.testbit_even_0.
 Qed.
 
 Lemma testbit_odd_succ : forall a n, 0<=n ->
  testbit (2*a+1) (succ n) = testbit a n.
 Proof.
- intros a n. zify. apply Ztestbit_odd_succ.
+ intros a n. zify. apply Z.testbit_odd_succ.
 Qed.
 
 Lemma testbit_even_succ : forall a n, 0<=n ->
  testbit (2*a) (succ n) = testbit a n.
 Proof.
- intros a n. zify. apply Ztestbit_even_succ.
+ intros a n. zify. apply Z.testbit_even_succ.
 Qed.
 
 Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false.
 Proof.
- intros a n. zify. apply Ztestbit_neg_r.
+ intros a n. zify. apply Z.testbit_neg_r.
 Qed.
 
 Lemma shiftr_spec : forall a n m, 0<=m ->
  testbit (shiftr a n) m = testbit a (m+n).
 Proof.
- intros a n m. zify. apply Zshiftr_spec.
+ intros a n m. zify. apply Z.shiftr_spec.
 Qed.
 
 Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m ->
  testbit (shiftl a n) m = testbit a (m-n).
 Proof.
  intros a n m. zify. intros Hn H.
- now apply Zshiftl_spec_high.
+ now apply Z.shiftl_spec_high.
 Qed.
 
 Lemma shiftl_spec_low : forall a n m, m<n ->
  testbit (shiftl a n) m = false.
 Proof.
- intros a n m. zify. intros H. now apply Zshiftl_spec_low.
+ intros a n m. zify. intros H. now apply Z.shiftl_spec_low.
 Qed.
 
 Lemma land_spec : forall a b n,
  testbit (land a b) n = testbit a n && testbit b n.
 Proof.
- intros a n m. zify. now apply Zand_spec.
+ intros a n m. zify. now apply Z.land_spec.
 Qed.
 
 Lemma lor_spec : forall a b n,
  testbit (lor a b) n = testbit a n || testbit b n.
 Proof.
- intros a n m. zify. now apply Zor_spec.
+ intros a n m. zify. now apply Z.lor_spec.
 Qed.
 
 Lemma ldiff_spec : forall a b n,
  testbit (ldiff a b) n = testbit a n && negb (testbit b n).
 Proof.
- intros a n m. zify. now apply Zdiff_spec.
+ intros a n m. zify. now apply Z.ldiff_spec.
 Qed.
 
 Lemma lxor_spec : forall a b n,
  testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
 Proof.
- intros a n m. zify. now apply Zxor_spec.
+ intros a n m. zify. now apply Z.lxor_spec.
 Qed.
 
 Lemma div2_spec : forall a, div2 a == shiftr a 1.
 Proof.
- intros a. zify. now apply Zdiv2_spec.
+ intros a. zify. now apply Z.div2_spec.
 Qed.
 
 End ZTypeIsZAxioms.