From a3ed8cd87d30a7539c14702f52710b899b9bf77b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Sep 2003 00:11:12 +0000
Subject: Mise en place des V8Notation et V8Infix pour déclarer des notations
 en v8 même si incompatible avec la syntaxe v7

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

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index d8766f2737..fd12e5c945 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -331,6 +331,13 @@ GEXTEND Gram
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
          VernacNotation (local,c,None,Some(s,modl),sc)
 
+     | IDENT "V8Infix"; local = locality; op8 = STRING; p = global;
+         modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
+	 sc = OPT [ ":"; sc = IDENT -> sc] ->
+           let (a8,n8,b) =
+             Metasyntax.interp_infix_modifiers None None modl in
+           VernacInfix (local,None,None,"",p,b,Some(a8,n8,op8),sc)
+
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
   ] ]
-- 
cgit v1.2.3