diff options
Diffstat (limited to 'parsing/g_vernac.ml4')
| -rw-r--r-- | parsing/g_vernac.ml4 | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index b4a7fce5b3..e8268e038d 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -355,13 +355,19 @@ GEXTEND Gram gallina_ext: [ [ (* Interactive module declaration *) - IDENT "Module"; id = base_ident; bl = module_binders_list; - mty_o = OPT of_module_type; mexpr_o = OPT is_module_expr -> - VernacDeclareModule (id, bl, mty_o, mexpr_o) + IDENT "Module"; id = base_ident; + bl = module_binders_list; mty_o = OPT of_module_type; + mexpr_o = OPT is_module_expr -> + VernacDefineModule (id, bl, mty_o, mexpr_o) | IDENT "Module"; "Type"; id = base_ident; bl = module_binders_list; mty_o = OPT is_module_type -> VernacDeclareModuleType (id, bl, mty_o) + + | IDENT "Declare"; IDENT "Module"; id = base_ident; + bl = module_binders_list; mty_o = OPT of_module_type; + mexpr_o = OPT is_module_expr -> + VernacDeclareModule (id, bl, mty_o, mexpr_o) (* This end a Section a Module or a Module Type *) |