diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index a78f4645c2..d534c107f1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -437,22 +437,18 @@ GRAMMAR EXTEND Gram rec_definition: [ [ id_decl = ident_decl; bl = binders_fixannot; - rtype = rec_type_cstr; + rtype = type_cstr; body_def = OPT [":="; def = lconstr -> { def } ]; notations = decl_notation -> { let binders, rec_order = bl in {fname = fst id_decl; univs = snd id_decl; rec_order; binders; rtype; body_def; notations} } ] ] ; corec_definition: - [ [ id_decl = ident_decl; binders = binders; rtype = rec_type_cstr; + [ [ id_decl = ident_decl; binders = binders; rtype = type_cstr; body_def = OPT [":="; def = lconstr -> { def }]; notations = decl_notation -> { {fname = fst id_decl; univs = snd id_decl; rec_order = (); binders; rtype; body_def; notations} } ]] ; - rec_type_cstr: - [ [ ":"; c=lconstr -> { c } - | -> { CAst.make ~loc @@ CHole (None, IntroAnonymous, None) } ] ] - ; (* Inductive schemes *) scheme: [ [ kind = scheme_kind -> { (None,kind) } |