diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 08:18:03 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 08:18:03 +0000 |
| commit | e9c8f69be0e0158d493b45476246cb82f7eb5d5a (patch) | |
| tree | 9f6f7fbbd844642daaa80b13407f97c8710c2c29 /parsing/g_constrnew.ml4 | |
| parent | f475ae32ed4ff6d4a48c6cbd94e2b6c28334ed42 (diff) | |
Passage de lconstr à constr pour les arguments immédiat de commandes
et tactiques; qqes bugs d'affichage; passage de la précédence des
projections de 10 à 9 avec associativité à gauche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_constrnew.ml4')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 573ac2dd3..700ac6734 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -153,7 +153,7 @@ GEXTEND Gram [ [ c = operconstr -> c ] ] ; constr: - [ [ c = operconstr LEVEL "9" -> c ] ] + [ [ c = operconstr LEVEL "9L" -> c ] ] ; tuple_constr: [ @@ -174,14 +174,12 @@ GEXTEND Gram [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ] | "10L" LEFTA [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(None,f),args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) - | c=operconstr; ".("; f=global; args1=LIST0 appl_arg; ")"; - args2=LIST0 appl_arg -> - CApp(loc,(Some (List.length args1+1),CRef f),args1@(c,None)::args2) - | c=operconstr; ".("; "@"; f=global; args1=LIST0 NEXT; ")"; - args2=LIST0 NEXT -> - CAppExpl(loc,(Some (List.length args1+1),f),args1@c::args2) ] - | "9" [ ] + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(None,f),args) ] + | "9L" LEFTA + [ c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> + CApp(loc,(Some (List.length args+1),CRef f),args@[c,None]) + | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT; ")" -> + CAppExpl(loc,(Some (List.length args+1),f),args@[c]) ] | "1L" LEFTA [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ] | "0" @@ -212,8 +210,8 @@ GEXTEND Gram | c=fix_constr -> c ] ] ; appl_arg: - [ [ "@"; n=INT; ":="; c=operconstr LEVEL "9" -> (c,Some(int_of_string n)) - | c=operconstr LEVEL "9" -> (c,None) ] ] + [ [ "@"; n=INT; ":="; c=constr -> (c,Some(int_of_string n)) + | c=constr -> (c,None) ] ] ; atomic_constr: [ [ g=global -> CRef g |