diff options
| author | herbelin | 2002-10-22 15:41:22 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-22 15:41:22 +0000 |
| commit | b64e6112b187edcd96816b1728aed6f4de233554 (patch) | |
| tree | cae32b973e2495507429dd0c6afce79f9fcef74d /parsing | |
| parent | 6dc2847536b74df5a4a2e28ba5a990d89b003296 (diff) | |
Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique; ajout d'une option 'level' pour Notation; utilisation de Notation pour sumor et sumbool
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3173 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index be3d3fe264..293d81590a 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -232,12 +232,17 @@ GEXTEND Gram | IDENT "Distfix"; a = entry_prec; n = natural; s = STRING; p = qualid; sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacDistfix (a,n,s,p,sc) | IDENT "Notation"; a = entry_prec; n = natural; s = STRING; c = constr; - sc = OPT [ ":"; sc = IDENT -> sc ] -> VernacNotation (a,n,s,c,sc) + precl = [ "("; l = LIST1 var_precedence SEP ","; ")" -> l | -> [] ]; + sc = OPT [ ":"; sc = IDENT -> sc ] -> + VernacNotation (a,n,s,c,precl,sc) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) ] ] ; + var_precedence: + [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> (x,n) ] ] + ; opt_scope: [ [ IDENT "_" -> None | sc = IDENT -> Some sc ] ] ; |