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, 8 insertions, 9 deletions

diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index c2a173e22a..1c06b0b8ed 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -56,7 +56,7 @@ Module Type ZType.
  Parameter div : t -> t -> t.
  Parameter modulo : t -> t -> t.
  Parameter quot : t -> t -> t.
- Parameter remainder : t -> t -> t.
+ Parameter rem : t -> t -> t.
  Parameter gcd : t -> t -> t.
  Parameter sgn : t -> t.
  Parameter abs : t -> t.
@@ -88,7 +88,7 @@ Module Type ZType.
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
  Parameter spec_quot: forall x y, [quot x y] = [x] ÷ [y].
- Parameter spec_remainder: forall x y, [remainder x y] = [x] rem [y].
+ Parameter spec_rem: forall x y, [rem x y] = Zrem [x] [y].
  Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 6a823a7324..62b79fc3a7 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -16,8 +16,7 @@ Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
- spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot
- spec_remainder
+ spec_pow spec_log2 spec_even spec_odd spec_gcd spec_quot spec_rem
  : zsimpl.
 
 Ltac zsimpl := autorewrite with zsimpl.
@@ -353,25 +352,25 @@ Definition mod_bound_pos :
 (** Quot / Rem *)
 
 Program Instance quot_wd : Proper (eq==>eq==>eq) quot.
-Program Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+Program Instance rem_wd : Proper (eq==>eq==>eq) rem.
 
-Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + (remainder a b).
+Theorem quot_rem : forall a b, ~b==0 -> a == b*(quot a b) + rem a b.
 Proof.
 intros a b _. zify. apply Z_quot_rem_eq.
 Qed.
 
 Theorem rem_bound_pos :
- forall a b, 0<=a -> 0<b -> 0 <= remainder a b /\ remainder a b < b.
+ forall a b, 0<=a -> 0<b -> 0 <= rem a b /\ rem a b < b.
 Proof.
 intros a b. zify. intros. now apply Zrem_bound.
 Qed.
 
-Theorem rem_opp_l : forall a b, ~b==0 -> remainder (-a) b == -(remainder a b).
+Theorem rem_opp_l : forall a b, ~b==0 -> rem (-a) b == -(rem a b).
 Proof.
 intros a b _. zify. apply Zrem_opp_l.
 Qed.
 
-Theorem rem_opp_r : forall a b, ~b==0 -> remainder a (-b) == remainder a b.
+Theorem rem_opp_r : forall a b, ~b==0 -> rem a (-b) == rem a b.
 Proof.
 intros a b _. zify. apply Zrem_opp_r.
 Qed.