Ajout V8Notation

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

3 files changed, 16 insertions, 8 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index f640622798..1bd70679ff 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -253,7 +253,11 @@ GEXTEND Gram
                let mv8 = match mv8 with
                    Some mv8 -> mv8
                  | _ -> List.map map_modl modl in
-	       VernacSyntaxExtension (local,s,modl,Some(s8,mv8))
+	       VernacSyntaxExtension (local,Some (s,modl),Some(s8,mv8))
+
+     | IDENT "Uninterpreted"; IDENT "V8Notation"; local = locality; s = STRING; 
+	 modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] ->
+	   VernacSyntaxExtension (local,None,Some(s,modl))
 
      | IDENT "Open"; local = locality; IDENT "Scope"; 
 	 sc = IDENT -> VernacOpenScope (local,sc)
@@ -294,7 +298,7 @@ GEXTEND Gram
      | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr;
 	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
 	       | -> [] ] ->
-	 VernacNotation (local,"'"^s^"'",c,l,None,None)
+	 VernacNotation (local,c,Some("'"^s^"'",l),None,None)
      | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ];
@@ -308,7 +312,11 @@ GEXTEND Gram
                let mv8 = match mv8 with
                    Some mv8 -> mv8
                  | _ -> List.map map_modl modl in
-               VernacNotation (local,s,c,modl,Some(s8,mv8),sc)
+               VernacNotation (local,c,Some(s,modl),Some(s8,mv8),sc)
+     | IDENT "V8Notation"; local = locality; s = STRING; ":="; c = constr;
+         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
+         VernacNotation (local,c,None,Some(s,modl),sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4865611a69..629c201775 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -424,7 +424,7 @@ GEXTEND Gram
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
 		 CApp (loc,c,l)
 	     | None -> c in
-	   VernacNotation (false,"'"^id^"'",c,[],None,None)
+	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
       | IDENT "Implicits"; qid = global -> VernacDeclareImplicits (qid,None)
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index 93de5a0e63..809ba58cfd 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -429,7 +429,7 @@ GEXTEND Gram
 		 let l = list_tabulate (fun _ -> (CHole (loc),None)) n in
 		 CApp (loc,c,l)
 	     | None -> c in
-	   VernacNotation (false,"'"^id^"'",c,[],None,None)
+	   VernacNotation (false,c,Some("'"^id^"'",[]),None,None)
 *)
       | IDENT "Implicits"; qid = global; "["; l = LIST0 natural; "]" ->
 	  VernacDeclareImplicits (qid,Some l)
@@ -678,11 +678,11 @@ GEXTEND Gram
      | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr;
 	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
 	       | -> [] ] ->
-	 VernacNotation (local,"'"^s^"'",c,l,None,None)
+	 VernacNotation (local,c,Some("'"^s^"'",l),None,None)
      | IDENT "Notation"; local = locality; s = STRING; ":="; c = constr;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-           VernacNotation (local,s,c,modl,None,sc)
+           VernacNotation (local,c,Some(s,modl),None,sc)
 
      | IDENT "Grammar"; IDENT "tactic"; IDENT "simple_tactic";
         OPT [ ":"; IDENT "tactic" ]; ":=";
@@ -698,7 +698,7 @@ GEXTEND Gram
 
      | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; 
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,s,l,None)
+	 -> VernacSyntaxExtension (local,Some(s,l),None)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)