diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-07 14:32:30 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-07 14:42:44 +0200 |
| commit | 8a7f111ad5ce35e183016a2a968d19f29b7622c5 (patch) | |
| tree | ef792aba6a02d9eb4a6234005c816ef72e8cc8f8 /parsing/g_vernac.ml4 | |
| parent | d37aab528dca587127b9f9944e1521e4fc3d9cc7 (diff) | |
Record fields accept an optional final semicolon separator.
There is no such thing as the OPTSEP macro in Camlp4 so I had
to expand it by hand.
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 63850713f..e9915fceb 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -325,9 +325,9 @@ GEXTEND Gram | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> Constructors ((c id)::l) | id = identref ; c = constructor_type -> Constructors [ c id ] - | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> + | cstr = identref; "{"; fs = record_fields; "}" -> RecordDecl (Some cstr,fs) - | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) + | "{";fs = record_fields; "}" -> RecordDecl (None,fs) | -> Constructors [] ] ] ; (* @@ -389,6 +389,13 @@ GEXTEND Gram [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ]; ntn = decl_notation -> (bd,pri),ntn ] ] ; + record_fields: + [ [ f = record_field; ";"; fs = record_fields -> f :: fs + | f = record_field; ";" -> [f] + | f = record_field -> [f] + | -> [] + ] ] + ; record_binder_body: [ [ l = binders; oc = of_type_with_opt_coercion; t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t)) |