diff options
| author | letouzey | 2013-07-17 15:31:36 +0000 |
|---|---|---|
| committer | letouzey | 2013-07-17 15:31:36 +0000 |
| commit | 3d09e39dd423d81c6af3e991d5b282ea8608646b (patch) | |
| tree | ae5e89db801b216b6152fb7d6bd0d7efe855ef57 /parsing | |
| parent | 9f3fc5d04b69f0c6bf6eec56c32ed11a218dde61 (diff) | |
More dynamic argument scopes
When arguments scopes are set manually, nothing new, they stay
as they are (until maybe another Arguments invocation).
But when argument scopes are computed out of the argument type and
the Bind Scope information, this kind of scope is now dynamic:
a later Bind Scope will be able to impact the scopes of an earlier
constant. For Instance:
Definition f (n:nat) := n.
About f. (* Argument scope is [nat_scope] *)
Bind Scope other_scope with nat.
About f. (* Argument scope is [other_scope] *)
This allows to get rid of hacks for modifying scopes during functor
applications. Moreover, the subst_arguments_scope is now
environment-insensitive (needed for forthcoming changes in declaremods).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 bc07fe8962..4504146258 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: |