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 | |
| parent | f69b14496b0783c2281db482682540b2e419b967 (diff) | |
[ast] [constrexpr] Make recursion_order_expr an AST node.
This is a bit more uniform.
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constr.mlg | 8 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 2 |
2 files changed, 5 insertions, 5 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 } ] ] diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 84d19730fa..3a57c14a3b 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -191,7 +191,7 @@ module Constr : val binder : local_binder_expr list Entry.t (* closed_binder or variable *) val binders : local_binder_expr list Entry.t (* list of binder *) val open_binders : local_binder_expr list Entry.t - val binders_fixannot : (local_binder_expr list * recursion_order_expr CAst.t option) Entry.t + val binders_fixannot : (local_binder_expr list * recursion_order_expr option) Entry.t val typeclass_constraint : (lname * bool * constr_expr) Entry.t val record_declaration : constr_expr Entry.t val appl_arg : (constr_expr * explicitation CAst.t option) Entry.t |