Suppression des surcharge de regles de grammaire en v7

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

3 files changed, 3 insertions, 5 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 0e254c8e59..4fa0d7273a 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -175,8 +175,7 @@ Definition negb := [b:bool]Cases b of
 Infix "||" orb  (at level 4, left associativity) : bool_scope.
 Infix "&&" andb (at level 3, no associativity) : bool_scope
   V8only (at level 30, left associativity).
-Notation "- b" := (negb b) (at level 0, right associativity) : bool_scope
-  V8only.
+Notation "- b" := (negb b) : bool_scope V8only
 
 Open Local Scope bool_scope.
 
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index d81dd968f8..d5055507b4 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -232,8 +232,7 @@ Module Z_scope.
 Infix LEFTA 4 "+" Zplus : Z_scope.
 Infix LEFTA 4 "-" Zminus : Z_scope.
 Infix LEFTA 3 "*" Zmult : Z_scope.
-Notation "- x" := (Zopp x) (at level 0) : Z_scope
-  V8only (at level 40).
+Notation "- x" := (Zopp x) : Z_scope V8only.
 Infix NONA 5 "<=" Zle : Z_scope.
 Infix NONA 5 "<"  Zlt : Z_scope.
 Infix NONA 5 ">=" Zge : Z_scope.
diff --git a/theories/ZArith/fast_integer.v b/theories/ZArith/fast_integer.v
index 180ab9fd2b..203d158309 100644
--- a/theories/ZArith/fast_integer.v
+++ b/theories/ZArith/fast_integer.v
@@ -64,7 +64,7 @@ with add_carry [x:positive]:positive -> positive := [y:positive]
   | xH      xH      => (xI xH)
   end.
 
-V7only [Infix LEFTA 4 "+" add : positive_scope.].
+V7only [Notation "x + y" := (add x y) : positive_scope.].
 V8Infix "+" add : positive_scope.
 
 Open Local Scope positive_scope.