diff options
| author | Emilio Jesus Gallego Arias | 2019-04-16 18:58:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-16 18:58:54 +0200 |
| commit | d5d556a31b0711845a1f9df83f9b0b75281c11b6 (patch) | |
| tree | 871b7e98ab648eb313639aafd18e89f9423221c5 /parsing/g_constr.mlg | |
| parent | f69b14496b0783c2281db482682540b2e419b967 (diff) | |
[ast] [constrexpr] Make recursion_order_expr an AST node.
This is a bit more uniform.
Diffstat (limited to 'parsing/g_constr.mlg')
| -rw-r--r-- | parsing/g_constr.mlg | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 7786155092..4a9190c10a 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -440,10 +440,10 @@ GRAMMAR EXTEND Gram ] ] ; fixannot: - [ [ "{"; IDENT "struct"; id=identref; "}" -> { CStructRec id } - | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CWfRec(id,rel) } + [ [ "{"; IDENT "struct"; id=identref; "}" -> { CAst.make ~loc @@ CStructRec id } + | "{"; IDENT "wf"; rel=constr; id=identref; "}" -> { CAst.make ~loc @@ CWfRec(id,rel) } | "{"; IDENT "measure"; m=constr; id=OPT identref; - rel=OPT constr; "}" -> { CMeasureRec (id,m,rel) } + rel=OPT constr; "}" -> { CAst.make ~loc @@ CMeasureRec (id,m,rel) } ] ] ; impl_name_head: @@ -452,7 +452,7 @@ GRAMMAR EXTEND Gram binders_fixannot: [ [ na = impl_name_head; assum = impl_ident_tail; bl = binders_fixannot -> { (assum na :: fst bl), snd bl } - | f = fixannot -> { [], Some (CAst.make ~loc f) } + | f = fixannot -> { [], Some f } | b = binder; bl = binders_fixannot -> { b @ fst bl, snd bl } | -> { [], None } ] ] |