diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-19 00:11:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-19 00:11:12 +0000 |
| commit | a3ed8cd87d30a7539c14702f52710b899b9bf77b (patch) | |
| tree | 726c3495a4426d2cf6ddc2f0577aefe43de6b129 /parsing | |
| parent | 97621f6e9c6a23a839bf0a2f28efec9434a158a8 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index d8766f273..fd12e5c94 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 *) ] ] |