diff options
| author | Emilio Jesus Gallego Arias | 2019-11-21 11:09:26 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-11-21 11:09:26 +0100 |
| commit | b680b06b31c27751a7d551d95839aea38f7fbea1 (patch) | |
| tree | d02df9495e125288434cb84667df89578eb61474 /vernac | |
| parent | b233d38a7a6a3e73f093c5c5ec00f1a7582e7668 (diff) | |
| parent | 3a3d361e1fa3ce9a074789405f46ed4c1fc67b2f (diff) | |
Merge PR #11103: Grammars: unification fix/cofix between constr/vernac + cleaning
Reviewed-by: ejgallego
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/g_vernac.mlg | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index a78f4645c2..61de1bfd26 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) } @@ -492,7 +488,6 @@ GRAMMAR EXTEND Gram ; record_fields: [ [ f = record_field; ";"; fs = record_fields -> { f :: fs } - | f = record_field; ";" -> { [f] } | f = record_field -> { [f] } | -> { [] } ] ] |