diff options
| author | herbelin | 2003-04-17 15:01:24 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-17 15:01:24 +0000 |
| commit | 5b318ca418ef27d1bf2b155bebbf2425f65b4f1f (patch) | |
| tree | b04fb45d1fd3e8fb6b4253a2acbd595754ec7dc6 /parsing/g_basevernac.ml4 | |
| parent | 95f8a0ac38cbd792a0b5d8006aac1ef1a9f70da8 (diff) | |
Ajout "at next level" dans Notation
Mise en place structure pour définir un objet en même temps que sa notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3939 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_basevernac.ml4')
| -rw-r--r-- | parsing/g_basevernac.ml4 | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 3db24bcd12..13d4a623bb 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -214,7 +214,7 @@ END (* automatic translation of levels *) let adapt_level n = n*10 let map_modl = function - | SetItemLevel(ids,n) -> SetItemLevel(ids,adapt_level n) + | SetItemLevel(ids,NumLevel n) -> SetItemLevel(ids,NumLevel (adapt_level n)) | SetLevel n -> SetLevel(adapt_level n) | m -> m @@ -305,11 +305,14 @@ GEXTEND Gram locality: [ [ IDENT "Local" -> true | -> false ] ] ; + level: + [ [ IDENT "level"; n = natural -> NumLevel n + | IDENT "next"; IDENT "level" -> NextLevel ] ] + ; syntax_modifier: - [ [ x = IDENT; IDENT "at"; IDENT "level"; n = natural -> - SetItemLevel ([x],n) - | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; IDENT "level"; - n = natural -> SetItemLevel (x::l,n) + [ [ x = IDENT; IDENT "at"; lev = level -> SetItemLevel ([x],lev) + | x = IDENT; ","; l = LIST1 IDENT SEP ","; IDENT "at"; lev = level -> + SetItemLevel (x::l,lev) | IDENT "at"; IDENT "level"; n = natural -> SetLevel n | IDENT "left"; IDENT "associativity" -> SetAssoc Gramext.LeftA | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA |