7 files changed, 29 insertions, 40 deletions
diff --git a/contrib/ring/Ring_theory.v b/contrib/ring/Ring_theory.v
index 55ad8023f3..b938f7db04 100644
--- a/contrib/ring/Ring_theory.v
+++ b/contrib/ring/Ring_theory.v
@@ -150,12 +150,10 @@ Infix 4 "+" Aplus V8only 50 (left associativity).
 Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- 0" := (Aopp Azero) (at level 0)
-  V8only (at level 50, left associativity).
-Notation "- 1" := (Aopp Aone) (at level 0)
-  V8only (at level 50, left associativity).
-Notation "- x" := (Aopp x) (at level 0)
-  V8only (at level 50, left associativity).
+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).
 
 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 c97536846b..eedc92197a 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -35,12 +35,10 @@ Infix 4 "+" Aplus V8only 50 (left associativity).
 Infix 4 "*" Amult V8only 40 (left associativity).
 Notation "0" := Azero.
 Notation "1" := Aone.
-Notation "- 0" := (Aopp Azero) (at level 0)
-  V8only (at level 50, left associativity).
-Notation "- 1" := (Aopp Aone) (at level 0)
-  V8only (at level 50, left associativity).
+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 50, left associativity).
+  V8only (at level 10, right associativity).
 
 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/interp/constrintern.ml b/interp/constrintern.ml
index 66851e70e8..97790d3633 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -586,9 +586,6 @@ let internalise sigma env allow_soapp lvar c =
     | CLetIn (loc,(_,na),c1,c2) ->
 	RLetIn (loc, na, intern (reset_tmp_scope env) c1,
           intern (push_name_env lvar env na) c2)
-    | CNotation (loc,"- _",[CNumeral(_,Bignat.POS p)]) ->
-	let scopes = option_cons tmp_scope scopes in
-        Symbols.interp_numeral loc (Bignat.NEG p) scopes
     | CNotation (loc,ntn,args) ->
 	let scopes = option_cons tmp_scope scopes in
 	let (ids,c) = Symbols.interp_notation ntn scopes in
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index d5d1db939e..ea736cc91f 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -178,9 +178,10 @@ GEXTEND Gram
     | "90" RIGHTA
       [ c1 = operconstr; "->"; c2 = binder_constr -> CArrow(loc,c1,c2)
       | c1 = operconstr; "->"; c2 = operconstr    -> CArrow(loc,c1,c2) ]
-    | "10" LEFTA
+    | "10"
       [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ]
+      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args)
+      | "-"; n=INT -> CNumeral (loc,Bignat.NEG (Bignat.of_string n)) ]
     | "9" [ ]
     | "1" LEFTA
       [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" ->
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 152141bfae..5380115e1e 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -547,7 +547,7 @@ let default_levels_v8 =
    100,Gramext.RightA;
    99,Gramext.RightA;
    90,Gramext.RightA;
-   10,Gramext.LeftA;
+   10,Gramext.RightA;
    9,Gramext.RightA;
    1,Gramext.LeftA;
    0,Gramext.RightA]
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index 00c35de84e..7fb43a703e 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -54,9 +54,10 @@ Uninterpreted Notation "x * y" (at level 3, right associativity)
 Uninterpreted V8Notation "x / y" (at level 40, left associativity).
 Uninterpreted Notation "x + y" (at level 4, left associativity).
 Uninterpreted Notation "x - y" (at level 4, left associativity).
-Uninterpreted Notation "- x" (at level 0) V8only (at level 50).
+Uninterpreted Notation "- x" (at level 0)
+  V8only (at level 10, right associativity).
 Uninterpreted Notation "/ x" (at level 0)
-  V8only (at level 40, left associativity).
+  V8only (at level 10, right associativity).
 
 Uninterpreted V8Notation "x ^ y" (at level 30, left associativity).
 
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 3929acdf9f..53f8aec077 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -205,37 +205,31 @@ Syntax constr
 (* For parsing/printing based on scopes *)
 Module R_scope.
 
-Infix "<=" Rle (at level 5, no associativity) : R_scope.
-Infix "<"  Rlt (at level 5, no associativity) : R_scope.
-Infix ">=" Rge (at level 5, no associativity) : R_scope.
-Infix ">" Rgt (at level 5, no associativity) : R_scope.
-Infix "+" Rplus (at level 4) : R_scope
-  V8only (at level 50, left associativity).
-Infix "-" Rminus (at level 4) : R_scope
-  V8only (at level 50, left associativity).
-Infix "*" Rmult (at level 3) : R_scope
-  V8only (at level 40, left associativity).
-Infix "/" Rdiv (at level 3) : R_scope
-  V8only (at level 40, left associativity).
-Notation "- x" := (Ropp x) (at level 0) : R_scope
-  V8only (at level 50, left associativity).
+Infix "<=" Rle (at level 5, no associativity) : R_scope V8only.
+Infix "<"  Rlt (at level 5, no associativity) : R_scope V8only.
+Infix ">=" Rge (at level 5, no associativity) : R_scope V8only.
+Infix ">" Rgt (at level 5, no associativity) : R_scope V8only.
+Infix "+" Rplus (at level 4) : R_scope V8only.
+Infix "-" Rminus (at level 4) : R_scope V8only.
+Infix "*" Rmult (at level 3) : R_scope V8only.
+Infix "/" Rdiv (at level 3) : R_scope V8only.
+Notation "- x" := (Ropp x) (at level 0) : R_scope V8only.
 Notation "x == y == z" := (eqT R x y)/\(eqT R y z)
-  (at level 5, y at level 4, no associtivity): R_scope
-  V8only "x = y = z" (at level 70, y at next level, no associativity).
+  (at level 5, y at level 4, no associtivity): R_scope.
 Notation "x <= y <= z" := (Rle x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 70, y at next level, no associativity).
+  V8only.
 Notation "x <= y < z" := (Rle x y)/\(Rlt y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 70, y at next level, no associativity).
+  V8only.
 Notation "x < y < z" := (Rlt x y)/\(Rlt y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 70, y at next level, no associativity).
+  V8only.
 Notation "x < y <= z" := (Rlt x y)/\(Rle y z)
   (at level 5, y at level 4) : R_scope
-  V8only (at level 70, y at next level, no associativity).
+  V8only.
 Notation "/ x" := (Rinv x) (at level 0): R_scope
-  V8only (at level 40, left associativity).
+  V8only.
 
 Open Local Scope R_scope.
 End R_scope.