diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 92ada3d748..125fd3f127 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -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. |