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, 4 insertions, 4 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 89fa8e1707..f177755fa0 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -88,19 +88,19 @@ Module Type ZDiv' (Z:ZAxiomsMiniSig) := NZDiv.NZDiv' Z <+ ZDivSpecific Z.
 *)
 
 Module Type QuotRem (Import A : Typ).
- Parameters Inline quot remainder : t -> t -> t.
+ Parameters Inline quot rem : t -> t -> t.
 End QuotRem.
 
 Module Type QuotRemNotation (A : Typ)(Import B : QuotRem A).
  Infix "÷" := quot (at level 40, left associativity).
- Infix "rem" := remainder (at level 40, no associativity).
+ Infix "rem" := rem (at level 40, no associativity).
 End QuotRemNotation.
 
 Module Type QuotRem' (A : Typ) := QuotRem A <+ QuotRemNotation A.
 
 Module Type QuotRemSpec (Import A : ZAxiomsMiniSig')(Import B : QuotRem' A).
  Declare Instance quot_wd : Proper (eq==>eq==>eq) quot.
- Declare Instance rem_wd : Proper (eq==>eq==>eq) remainder.
+ Declare Instance rem_wd : Proper (eq==>eq==>eq) B.rem.
  Axiom quot_rem : forall a b, b ~= 0 -> a == b*(a÷b) + (a rem b).
  Axiom rem_bound_pos : forall a b, 0<=a -> 0<b -> 0 <= a rem b < b.
  Axiom rem_opp_l : forall a b, b ~= 0 -> (-a) rem b == - (a rem b).
diff --git a/theories/Numbers/Integer/Abstract/ZDivTrunc.v b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
index 37a0057edb..e33265762f 100644
--- a/theories/Numbers/Integer/Abstract/ZDivTrunc.v
+++ b/theories/Numbers/Integer/Abstract/ZDivTrunc.v
@@ -35,7 +35,7 @@ Module Type ZQuotProp
 
  Module Quot2Div <: NZDiv A.
   Definition div := quot.
-  Definition modulo := remainder.
+  Definition modulo := A.rem.
   Definition div_wd := quot_wd.
   Definition mod_wd := rem_wd.
   Definition div_mod := quot_rem.