Autour du parsing:

- Utilisation de notations de type "abbreviation paramétrée" plutôt que
  de notations introduisant des mots-clés, là où c'est possible (cela affecte
  QDen, in_left/in_right, inhabited, S/P dans NZCyclic).
- Extension du lexeur pour qu'il prenne le plus long token valide au
  lieu d'échouer sur un plus long préfixe non valide de token (permet
  notamment de faire passer la notation de Georges "'C_ G ( A )"
  sans invalider toute séquence commençant par 'C et non suivie de _)
- Rajout d'un point final à certains messages d'erreur qui n'en avaient pas.
- Ajout String.copy dans string_of_label ("trou" de mutabilité signalé
  par Georges -- le "trou" lié aux vecteurs des noeuds App restant lui
  ouvert).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11225 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 92ada3d74..125fd3f12 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.