diff options
Diffstat (limited to 'parsing/g_constrnew.ml4')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4 index 88d108fdd..1876863d4 100644 --- a/parsing/g_constrnew.ml4 +++ b/parsing/g_constrnew.ml4 @@ -142,11 +142,15 @@ GEXTEND Gram | "40L" LEFTA [ "-"; c = operconstr -> CNotation(loc,"- _",[c]) ] | "10L" LEFTA - [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,f,args) - | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,f,args) ] + [ f=operconstr; args=LIST1 appl_arg -> CApp(loc,(false,f),args) + | "@"; f=global; args=LIST0 NEXT -> CAppExpl(loc,(false,f),args) ] | "9" [ ] | "1L" LEFTA - [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) ] + [ c=operconstr; "%"; key=IDENT -> CDelimiters (loc,key,c) + | c=operconstr; ".("; f=global; args=LIST0 appl_arg; ")" -> + CApp(loc,(true,CRef f),args@[c,None]) + | c=operconstr; ".("; "@"; f=global; args=LIST0 NEXT -> + CAppExpl(loc,(false,f),args@[c]) ] | "0" [ c=atomic_constr -> c | c=match_constr -> c |