Division: avoid imposing rem as an infix keyword in Z_scope and bigZ_scope.

 No infix notation "rem" for Zrem (that will probably become Z.rem in
 a close future). This way, we avoid conflict with people already using
 rem for their own need. Same for BigZ. We still use infix rem, but
 only in the abstract layer of Numbers, in a way that doesn't inpact
 the rest of Coq. Btw, the axiomatized function is now named rem
 instead of remainder.

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

2 files changed, 5 insertions, 6 deletions

diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 72137eccf..6153ccc75 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -65,7 +65,7 @@ Arguments Scope BigZ.sqrt [bigZ_scope].
 Arguments Scope BigZ.div_eucl [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.modulo [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.quot [bigZ_scope bigZ_scope].
-Arguments Scope BigZ.remainder [bigZ_scope bigZ_scope].
+Arguments Scope BigZ.rem [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 Arguments Scope BigZ.even [bigZ_scope].
 Arguments Scope BigZ.odd [bigZ_scope].
@@ -92,7 +92,6 @@ Notation "x <= y < z" := (x<=y /\ y<z)%bigZ : bigZ_scope.
 Notation "x <= y <= z" := (x<=y /\ y<=z)%bigZ : bigZ_scope.
 Notation "[ i ]" := (BigZ.to_Z i) : bigZ_scope.
 Infix "mod" := BigZ.modulo (at level 40, no associativity) : bigZ_scope.
-Infix "rem" := BigZ.remainder (at level 40, no associativity) : bigZ_scope.
 Infix "÷" := BigZ.quot (at level 40, left associativity) : bigZ_scope.
 
 Local Open Scope bigZ_scope.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index f4baf32bc..4c4eb6c10 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -461,7 +461,7 @@ Module Make (N:NType) <: ZType.
   | Neg nx, Neg ny => Pos (N.div nx ny)
   end.
 
- Definition remainder x y :=
+ Definition rem x y :=
   if eq_bool y zero then x
   else
     match x, y with
@@ -478,10 +478,10 @@ Module Make (N:NType) <: ZType.
    rewrite Zquot_Zdiv_pos; trivial using N.spec_pos.
  Qed.
 
- Lemma spec_remainder : forall x y,
-   to_Z (remainder x y) = (to_Z x) rem (to_Z y).
+ Lemma spec_rem : forall x y,
+   to_Z (rem x y) = Zrem (to_Z x) (to_Z y).
  Proof.
-  intros x y. unfold remainder. rewrite spec_eq_bool, spec_0.
+  intros x y. unfold rem. rewrite spec_eq_bool, spec_0.
   assert (Hy := Zeq_bool_if (to_Z y) 0). destruct Zeq_bool.
   now rewrite Hy, Zrem_0_r.
   destruct x as [x|x], y as [y|y]; simpl in *; symmetry;