ZArith: for uniformity, Zdiv2 becomes Zquot2 while Zdiv2' becomes Zdiv2

 Now we have:
  - Zdiv and Zdiv2 : round toward bottom, no easy sign rule, remainder
    of a/2 is 0 or 1, operations related with two's-complement Zshiftr.
  - Zquot and Zquot2 : round toward zero, Zquot2 (-a) = - Zquot2 a,
    remainder of a/2 is 0 or Zsgn a.

 Ok, I'm introducing an incompatibility here, but I think coherence is
 really desirable. Anyway, people using Zdiv on positive numbers only
 shouldn't even notice the change. Otherwise, it's just a matter of
 sed -e "s/div2/quot2/g".

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

4 files changed, 6 insertions, 6 deletions

diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 1327c1923..7534628fa 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -719,9 +719,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) = Zdiv2 (to_Z x).
  Proof.
-  intros x. unfold div2. now rewrite spec_shiftr, Zdiv2'_spec, spec_1.
+  intros x. unfold div2. now rewrite spec_shiftr, Zdiv2_spec, spec_1.
  Qed.
 
 End Make.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index eab33051d..8ed42ed8d 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -202,7 +202,7 @@ Definition land_spec := Zand_spec.
 Definition lor_spec := Zor_spec.
 Definition ldiff_spec := Zdiff_spec.
 Definition lxor_spec := Zxor_spec.
-Definition div2_spec := Zdiv2'_spec.
+Definition div2_spec := Zdiv2_spec.
 
 Definition testbit := Ztestbit.
 Definition shiftl := Zshiftl.
@@ -211,7 +211,7 @@ Definition land := Zand.
 Definition lor := Zor.
 Definition ldiff := Zdiff.
 Definition lxor := Zxor.
-Definition div2 := Zdiv2'.
+Definition div2 := Zdiv2.
 
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index c33915449..788ca8e56 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -109,7 +109,7 @@ Module Type ZType.
  Parameter spec_lor: forall x y, [lor x y] = Zor [x] [y].
  Parameter spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y].
  Parameter spec_lxor: forall x y, [lxor x y] = Zxor [x] [y].
- Parameter spec_div2: forall x, [div2 x] = Zdiv2' [x].
+ Parameter spec_div2: forall x, [div2 x] = Zdiv2 [x].
 
 End ZType.
 
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index f8fa84283..8c1e7b4fa 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -471,7 +471,7 @@ Qed.
 
 Lemma div2_spec : forall a, div2 a == shiftr a 1.
 Proof.
- intros a. zify. now apply Zdiv2'_spec.
+ intros a. zify. now apply Zdiv2_spec.
 Qed.
 
 End ZTypeIsZAxioms.