diff options
| author | Hugo Herbelin | 2019-11-12 09:32:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-19 20:45:22 +0100 |
| commit | e7b29adca3c2ff636ff277dab843d517894f3bf6 (patch) | |
| tree | bad5adadc9fd93f6bfdd1c826538162478486713 /vernac | |
| parent | d10e7cc978a2abd97377c6365cc5366cf5cdf5eb (diff) | |
Grammar: mini-factorization between fix/cofix and Fixpoint/CoFixpoint.
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) } |