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

3 files changed, 4 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index a55fb5900..105cf0620 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -1593,10 +1593,10 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition div2 x := shiftr x one.
 
- Lemma spec_div2: forall x, [div2 x] = Zdiv2' [x].
+ Lemma spec_div2: forall x, [div2 x] = Zdiv2 [x].
  Proof.
   intros. unfold div2. symmetry.
-  rewrite spec_shiftr, spec_1. apply Zdiv2'_spec.
+  rewrite spec_shiftr, spec_1. apply Zdiv2_spec.
  Qed.
 
  (** TODO : provide efficient versions instead of just converting
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 021ac29ee..f186c55b4 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -99,7 +99,7 @@ Module Type NType.
  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 NType.
 
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index a169c009d..175b1ad2c 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -408,7 +408,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.
 
 (** Recursion *)