From 9b6517c0c933fb1d66c7feb53fa57e1697d8124a Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 7 Jan 2010 15:32:49 +0000 Subject: 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 --- parsing/g_vernac.ml4 | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) (limited to 'parsing/g_vernac.ml4') 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 -- cgit v1.2.3