diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 22f6d95b..fb3f0cef 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -8,7 +8,7 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NZCyclic.v 11040 2008-06-03 00:04:16Z letouzey $ i*) +(*i $Id: NZCyclic.v 11238 2008-07-19 09:34:03Z herbelin $ i*) Require Export NZAxioms. Require Import BigNumPrelude. @@ -89,8 +89,8 @@ Open Local Scope IntScope. Notation "x == y" := (NZeq x y) (at level 70) : IntScope. Notation "x ~= y" := (~ NZeq x y) (at level 70) : IntScope. Notation "0" := NZ0 : IntScope. -Notation "'S'" := NZsucc : IntScope. -Notation "'P'" := NZpred : IntScope. +Notation S x := (NZsucc x). +Notation P x := (NZpred x). (*Notation "1" := (S 0) : IntScope.*) Notation "x + y" := (NZadd x y) : IntScope. Notation "x - y" := (NZsub x y) : IntScope. |