Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x'

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

4 files changed, 4 insertions, 4 deletions

diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index b938f7db04..4281505e73 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -153,7 +153,7 @@ Notation "1" := Aone.
 Notation "- 0" := (Aopp Azero) (at level 0) V8only (at level 10).
 Notation "- 1" := (Aopp Aone) (at level 0) V8only (at level 10).
 Notation "- x" := (Aopp x) (at level 0) 
-  V8only (at level 10, right associativity).
+  V8only (at level 10, x at level 0).
 
 Record Ring_Theory : Prop :=
 { Th_plus_sym  : (n,m:A) n + m == m + n;
diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index eedc92197a..d31dd69951 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -38,7 +38,7 @@ Notation "1" := Aone.
 Notation "- 0" := (Aopp Azero) (at level 0) V8only (at level 10).
 Notation "- 1" := (Aopp Aone) (at level 0) V8only (at level 10).
 Notation "- x" := (Aopp x) (at level 0)
-  V8only (at level 10, right associativity).
+  V8only (at level 10, x at level 0).
 
 Variable plus_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a+a1 == a0+a2.
 Variable mult_morph : (a,a0,a1,a2:A) a == a0 -> a1 == a2 -> a*a1 == a0*a2.
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 984bd77c4f..3d0a7a2f10 100755
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -175,7 +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 40, left associativity).
-Notation "- b" := (negb b) : bool_scope V8only.
+V8Notation "- b" := (negb b) : bool_scope.
 
 Open Local Scope bool_scope.
 
diff --git a/theories/ZArith/Zsyntax.v b/theories/ZArith/Zsyntax.v
index 2805406a34..6c632ea42a 100644
--- a/theories/ZArith/Zsyntax.v
+++ b/theories/ZArith/Zsyntax.v
@@ -232,7 +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) : Z_scope V8only.
+Notation "- x" := (Zopp x) (at level 0): Z_scope V8only.
 Infix NONA 5 "<=" Zle : Z_scope.
 Infix NONA 5 "<"  Zlt : Z_scope.
 Infix NONA 5 ">=" Zge : Z_scope.