From e52a9fa8835eddf70d0c8e454470fb12eebef7cd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 30 Oct 2003 14:29:39 +0000
Subject: Parsing du moins unaire au niveau de l'application qui n'a pas besoin
 d'etre associative a gauche; gestion du signe dans le parseur pas dans
 l'interpreteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Ring_theory.v        | 10 ++++------
 contrib/ring/Setoid_ring_theory.v |  8 +++-----
 2 files changed, 7 insertions(+), 11 deletions(-)

(limited to 'contrib')

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.
-- 
cgit v1.2.3