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

3 files changed, 6 insertions, 5 deletions

diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v
index 57ed3ec2d1..c007686caf 100644
--- a/theories/Lists/PolyList.v
+++ b/theories/Lists/PolyList.v
@@ -47,7 +47,7 @@ Fixpoint app [l:list] : list -> list
                  end.
 
 Infix RIGHTA 7 "^" app : list_scope
-  V8only 45.
+  V8only RIGHTA 45.
 
 Lemma app_nil_end : (l:list)l=(l^nil).
 Proof. 
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v
index b469b94f4f..e84398b517 100644
--- a/theories/Lists/PolyListSyntax.v
+++ b/theories/Lists/PolyListSyntax.v
@@ -14,5 +14,6 @@ Require PolyList.
 
 V8Infix "::" cons (at level 45, right associativity) : list_scope.
 
-Infix RIGHTA 7 "^" app (* : list_scope *)
-  V8only 45.
+Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45.
+
+Open Scope list_scope.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index eee40d6938..bcf5a05915 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -286,8 +286,8 @@ Syntax constr
 ].
 
 
-Infix 3 "/" Zdiv (no associativity) : Z_scope V8only (left associativity).
-Infix 3 "mod" Zmod (no associativity) : Z_scope V8only (left associativity).
+Infix 3 "/" Zdiv (no associativity) : Z_scope V8only.
+Infix 3 "mod" Zmod (no associativity) : Z_scope.
 
 (** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *)