diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:49 +0000 |
| commit | 9b6517c0c933fb1d66c7feb53fa57e1697d8124a (patch) | |
| tree | d914d6bc2c5598baad03807ce40ada0b1d56045d /parsing/g_vernac.ml4 | |
| parent | e3e6ff629e258269bc9fe06f7be99a2d5f334071 (diff) | |
Include can accept both Module and Module Type
Syntax Include Type is still active, but deprecated, and triggers a warning.
The syntax M <+ M' <+ M'', which performs internally an Include, also
benefits from this: M, M', M'' can be independantly modules or module type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12640 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 4672a732a..f4d588b57 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -397,9 +397,10 @@ GEXTEND Gram | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl) | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl) | IDENT "Include"; e = module_expr; l = LIST0 ext_module_expr -> - VernacInclude(CIME(e::l)) + VernacInclude(e::l) | IDENT "Include"; "Type"; e = module_type; l = LIST0 ext_module_type -> - VernacInclude(CIMTE(e::l)) ] ] + warning "Include Type is deprecated; use Include instead"; + VernacInclude(e::l) ] ] ; export_token: [ [ IDENT "Import" -> Some false @@ -440,11 +441,11 @@ GEXTEND Gram (* Module expressions *) module_expr: [ [ me = module_expr_atom -> me - | me1 = module_expr; me2 = module_expr_atom -> CMEapply (me1,me2) + | me1 = module_expr; me2 = module_expr_atom -> CMapply (me1,me2) ] ] ; module_expr_atom: - [ [ qid = qualid -> CMEident qid | "("; me = module_expr; ")" -> me ] ] + [ [ qid = qualid -> CMident qid | "("; me = module_expr; ")" -> me ] ] ; with_declaration: [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> @@ -454,10 +455,10 @@ GEXTEND Gram ] ] ; module_type: - [ [ qid = qualid -> CMTEident qid + [ [ qid = qualid -> CMident qid | "("; mt = module_type; ")" -> mt - | mty = module_type; me = module_expr_atom -> CMTEapply (mty,me) - | mty = module_type; "with"; decl = with_declaration -> CMTEwith (mty,decl) + | mty = module_type; me = module_expr_atom -> CMapply (mty,me) + | mty = module_type; "with"; decl = with_declaration -> CMwith (mty,decl) ] ] ; END |