diff options
Diffstat (limited to 'vernac/g_vernac.mlg')
| -rw-r--r-- | vernac/g_vernac.mlg | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 2b475f1ef9..678d4436d2 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -402,16 +402,18 @@ GRAMMAR EXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident_decl; + [ [ id_decl = ident_decl; bl = binders_fixannot; - ty = type_cstr; - def = OPT [":="; def = lconstr -> { def } ]; ntn = decl_notation -> - { let bl, annot = bl in ((id,annot,bl,ty,def),ntn) } ] ] + rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> + { let binders, rec_order = bl in + {id_decl; rec_order; binders; rtype; body_def; notations} + } ] ] ; corec_definition: - [ [ id = ident_decl; bl = binders; ty = type_cstr; - def = OPT [":="; def = lconstr -> { def }]; ntn = decl_notation -> - { ((id,bl,ty,def),ntn) } ] ] + [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; + body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> + { {id_decl; rec_order=(); binders; rtype; body_def; notations} } ] ] ; type_cstr: [ [ ":"; c=lconstr -> { c } |