diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 29 |
1 files changed, 8 insertions, 21 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index bc07fe896..450414625 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -455,32 +455,19 @@ GEXTEND Gram | -> [] ] ] ; functor_app_annot: - [ [ IDENT "inline"; "at"; IDENT "level"; i = INT -> - [InlineAt (int_of_string i)], [] - | IDENT "no"; IDENT "inline" -> [NoInline], [] - | IDENT "scope"; sc1 = IDENT; IDENT "to"; sc2 = IDENT -> [], [sc1,sc2] - ] ] - ; - functor_app_annots: - [ [ "["; l = LIST1 functor_app_annot SEP ","; "]" -> - let inl,scs = List.split l in - let inl = match List.concat inl with - | [] -> DefaultInline - | [inl] -> inl - | _ -> error "Functor application with redundant inline annotations" - in { ann_inline = inl; ann_scope_subst = List.concat scs } - | -> { ann_inline = DefaultInline; ann_scope_subst = [] } + [ [ "["; IDENT "inline"; "at"; IDENT "level"; i = INT; "]" -> + InlineAt (int_of_string i) + | "["; IDENT "no"; IDENT "inline"; "]" -> NoInline + | -> DefaultInline ] ] ; module_expr_inl: - [ [ "!"; me = module_expr -> - (me, { ann_inline = NoInline; ann_scope_subst = []}) - | me = module_expr; a = functor_app_annots -> (me,a) ] ] + [ [ "!"; me = module_expr -> (me,NoInline) + | me = module_expr; a = functor_app_annot -> (me,a) ] ] ; module_type_inl: - [ [ "!"; me = module_type -> - (me, { ann_inline = NoInline; ann_scope_subst = []}) - | me = module_type; a = functor_app_annots -> (me,a) ] ] + [ [ "!"; me = module_type -> (me,NoInline) + | me = module_type; a = functor_app_annot -> (me,a) ] ] ; (* Module binder *) module_binder: |