diff options
| author | Arnaud Spiwack | 2014-09-03 18:22:58 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-04 10:25:55 +0200 |
| commit | 3c29ea3b2e58a7f76195834e9ab43d7e99a0a323 (patch) | |
| tree | 4b45017a8432cba1d1fa26bebfdc5f5a1619f549 | |
| parent | a93104d5462894d5d0651aa2e04e12c311eb5897 (diff) | |
Factorize the parsing rules of [Record] and the other kind of type definitions.
They were almost identical, except some unused misplaced coercion symbol in the non-[Record] rule.
| -rw-r--r-- | parsing/g_vernac.ml4 | 29 |
1 files changed, 10 insertions, 19 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index f7f049884b..9fb7c89261 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -220,17 +220,6 @@ GEXTEND Gram ] ] ; - gallina_ext: - [ [ priv = private_token; - b = record_token; oc = opt_coercion; name = identref; - ps = binders; - s = OPT [ ":"; s = lconstr -> s ]; - cfs = [ ":="; l = constructor_list_or_record_decl -> l - | -> RecordDecl (None, []) ] -> - let (recf,indf) = b in - VernacInductive (priv,indf,[((oc,name),ps,s,recf,cfs),[]]) - ] ] - ; thm_token: [ [ "Theorem" -> Theorem | IDENT "Lemma" -> Lemma @@ -270,16 +259,14 @@ GEXTEND Gram finite_token: [ [ "Inductive" -> (Inductive_kw,Finite) | "CoInductive" -> (CoInductive,CoFinite) - | "Variant" -> (Variant,BiFinite) ] ] + | "Variant" -> (Variant,BiFinite) + | IDENT "Record" -> (Record,BiFinite) + | IDENT "Structure" -> (Structure,BiFinite) + | IDENT "Class" -> (Class true,BiFinite) ] ] ; private_token: [ [ IDENT "Private" -> true | -> false ] ] ; - record_token: - [ [ IDENT "Record" -> (Record,BiFinite) - | IDENT "Structure" -> (Structure,BiFinite) - | IDENT "Class" -> (Class true,BiFinite) ] ] - ; (* Simple definitions *) def_body: [ [ bl = binders; ":="; red = reduce; c = lconstr -> @@ -304,10 +291,14 @@ GEXTEND Gram | -> [] ] ] ; (* Inductives and records *) + opt_constructors_or_fields: + [ [ ":="; lc = constructor_list_or_record_decl -> lc + | -> RecordDecl (None, []) ] ] + ; inductive_definition: - [ [ id = identref; oc = opt_coercion; indpar = binders; + [ [ oc = opt_coercion; id = identref; indpar = binders; c = OPT [ ":"; c = lconstr -> c ]; - ":="; lc = constructor_list_or_record_decl; ntn = decl_notation -> + lc=opt_constructors_or_fields; ntn = decl_notation -> (((oc,id),indpar,c,lc),ntn) ] ] ; constructor_list_or_record_decl: |