diff options
author | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2008-08-08 13:18:42 +0200 |
commit | 870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch) | |
tree | 0c647056de1832cf1dba5ba58758b9121418e4be /theories/Numbers/Cyclic | |
parent | a0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff) |
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'theories/Numbers/Cyclic')
-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. |