From f2fdab57784b34bab5ef7e0c9d34fee76c329a33 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 1 Nov 2003 22:03:52 +0000
Subject: 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
---
 contrib/ring/Ring_theory.v        | 2 +-
 contrib/ring/Setoid_ring_theory.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib')

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