Heritage des notations v7 seulement si zero information v8

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4749 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 3 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index e4ce693c2..998a6d2c4 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -312,9 +312,17 @@ GEXTEND Gram
 		let mv = Metasyntax.merge_modifiers a n modl in
 		let v8 = Util.option_app (function (op8,mv8) ->
 		  let op8 = match op8 with None -> op | Some op -> op in
-		  let mv8 = if mv8=[] then List.map map_modl mv else mv8 in
-		  let mv8 = if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then SetLevel 10 :: mv8 else mv8 in
-		  let mv8 = if List.for_all (function SetAssoc _ -> false | _ -> true) mv8 then SetAssoc Gramext.LeftA :: mv8 else mv8 in
+		  let mv8 =
+		    if mv8=[] then
+		      let mv8 = List.map map_modl mv in
+		      let mv8 =	if List.for_all
+			(function SetLevel _ -> false | _ -> true) mv8
+		      then SetLevel 10 :: mv8 else mv8 in
+		      let mv8 = if List.for_all
+			(function SetAssoc _ -> false | _ -> true) mv8
+		      then SetAssoc Gramext.LeftA :: mv8 else mv8 in
+		      mv8
+		  else mv8 in
 		  (op8,mv8)) mv8 in
 		VernacInfix (local,(op,mv),p,v8,sc)
      | IDENT "Distfix"; local = locality; a = entry_prec; n = natural;