From 66eed5340efdfbd41a775cf679213507bb2ac424 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 Apr 2003 16:49:47 +0000
Subject: Prise en compte des syntaxes v8 dans Uninterpreted Notation Suite
 mise en place infrastructure pour déclaration de syntaxe simultanée  à la
 déclaration d'inductifs Table séparée pour les précédences de notations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3983 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_basevernac.ml4 | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 5817268912..f640622798 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -242,8 +242,18 @@ GEXTEND Gram
          VernacSyntax (u,el)
 
      | IDENT "Uninterpreted"; IDENT "Notation"; local = locality; s = STRING; 
-	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]
-	 -> VernacSyntaxExtension (local,s,l)
+	 modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+         (s8,mv8) =
+             [IDENT "V8only";
+              s8=OPT STRING;
+              mv8=OPT["(";mv8=LIST1 syntax_modifier SEP ","; ")" -> mv8] ->
+                (s8,mv8)
+             | -> (None,None)] ->
+               let s8 = match s8 with Some s -> s | _ -> s in
+               let mv8 = match mv8 with
+                   Some mv8 -> mv8
+                 | _ -> List.map map_modl modl in
+	       VernacSyntaxExtension (local,s,modl,Some(s8,mv8))
 
      | IDENT "Open"; local = locality; IDENT "Scope"; 
 	 sc = IDENT -> VernacOpenScope (local,sc)
-- 
cgit v1.2.3