diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-16 17:27:17 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-16 17:27:17 +0000 |
| commit | e216c2de60d1d8b1fd35169257349fa4c257a516 (patch) | |
| tree | e3ba078fa4bb837c8708f6f8673f3438ec0e6526 /theories/Numbers/Integer/Binary | |
| parent | b9f4f52371fef6c94a0b2de4784aefe95c793a51 (diff) | |
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
Diffstat (limited to 'theories/Numbers/Integer/Binary')
| -rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index f68aa0dbe..5f38d57b8 100644 --- a/theories/Numbers/Integer/Binary/ZBinary.v +++ b/theories/Numbers/Integer/Binary/ZBinary.v @@ -189,7 +189,7 @@ Definition rem_bound_pos := Zrem_bound. Definition rem_opp_l := fun a b (_:b<>0) => Zrem_opp_l a b. Definition rem_opp_r := fun a b (_:b<>0) => Zrem_opp_r a b. Definition quot := Zquot. -Definition remainder := Zrem. +Definition rem := Zrem. (** We define [eq] only here to avoid refering to this [eq] above. *) |