From 8ed294710b082e8331efe0a592de0afabb701bfd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 21 Sep 2003 22:50:38 +0000
Subject: Changement de la politique de V8only: V8only tout seul signifie
 'seulement interprétation' en V8; héritage des paramêtres de V7 seulement si
 pas V8only; sinon, il faut tout expliciter (pas d'héritage partiel)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4433 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/ring/Setoid_ring_theory.v | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'contrib')

diff --git a/contrib/ring/Setoid_ring_theory.v b/contrib/ring/Setoid_ring_theory.v
index 021e2d1414..8b9ae52f0f 100644
--- a/contrib/ring/Setoid_ring_theory.v
+++ b/contrib/ring/Setoid_ring_theory.v
@@ -18,8 +18,7 @@ Section Setoid_rings.
 Variable A : Type.
 Variable Aequiv : A -> A -> Prop.
 
-Infix "==" Aequiv (at level 5)
-  V8only (at level 50).
+Infix Local "==" Aequiv (at level 5, no associativity).
 
 Variable S : (Setoid_Theory A Aequiv).
 
-- 
cgit v1.2.3