summaryrefslogtreecommitdiff
path: root/theories/Numbers/Cyclic
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/Cyclic')
-rw-r--r--theories/Numbers/Cyclic/Abstract/NZCyclic.v6
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.