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

5 files changed, 36 insertions, 24 deletions

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).
 
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index fd12e5c945..b3988f1e02 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -282,24 +282,27 @@ GEXTEND Gram
          p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc];
-         (op8,nv8,mv8) =
+         mv8 =
               [IDENT "V8only";
-               op8=OPT STRING;
+               a8=entry_prec;
                n8=OPT natural;
                mv8=OPT["("; l = LIST1 syntax_modifier SEP ","; ")" -> l] ->
-                    (op8,n8,mv8)
-              | -> (None,None,None)] ->
+		 (match (a8,n8,mv8) with
+		   | None,None,None -> None
+		   | _,_,Some mv8 ->
+		   let (a8,n8,_) = Metasyntax.interp_infix_modifiers a8 n8 mv8
+		   in Some(a8,n8)
+		   | _,_,None -> Some (a8,n8))
+              | -> (* Means: rules are based on V7 rules *)
+		  Some (None,None) ] ->
+		let v8 = Util.option_app (function
+		  | None, None ->
+		      let nv8 = Util.option_app adapt_level n in
+		      let mv8 = List.map map_modl modl in
+		      let (a8,n8,_) = Metasyntax.interp_infix_modifiers a nv8
+			mv8 in (a8,n8,op)
+		  | a8,n8 -> (a8,n8,op)) mv8 in
            let (ai,ni,b) = Metasyntax.interp_infix_modifiers a n modl in
-           let op8 = match op8 with Some s -> s | _ -> op in
-           let nv8 = match nv8 with
-               Some n -> Some n
-             | _ -> Util.option_app adapt_level n in
-           let mv8 = match mv8 with
-               Some m -> m
-             | _ -> List.map map_modl modl in
-           let (a8,n8,_) =
-             Metasyntax.interp_infix_modifiers a nv8 mv8 in
-           let v8 = Some(a8,n8,op8) in
            VernacInfix (local,ai,ni,op,p,b,v8,sc)
      | IDENT "Distfix"; local = locality; a = entry_prec; n = natural; 
 	   s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
@@ -319,13 +322,22 @@ GEXTEND Gram
              [IDENT "V8only";
               s8=OPT STRING;
               mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
-                (s8,mv8)
-             | -> (None,None)] ->
+		(s8,mv8)
+             | -> (* Means: rules are based on V7 rules *)
+		 None, Some [] ] ->
+(*
                let s8 = match s8 with Some s -> s | _ -> s in
                let mv8 = match mv8 with
                    Some mv8 -> mv8
                  | _ -> List.map map_modl modl in
-               VernacNotation (local,c,Some(s,modl),Some(s8,mv8),sc)
+*)
+	       let smv8 = match s8,mv8 with
+		 | None, None -> None   (* = only interpretation *)
+		 | Some s8, None -> Some (s8,[]) (* = only interp, new s *)
+		 | None, Some [] -> Some (s,List.map map_modl modl) (*like v7*)
+		 | None, Some mv8 -> Some (s,mv8) (* s like v7 *)
+		 | Some s8, Some mv8 -> Some (s8,mv8) in
+               VernacNotation (local,c,Some(s,modl),smv8,sc)
      | IDENT "V8Notation"; local = locality; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
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]). *)