diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/vernacentries.ml | 12 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 2 |
2 files changed, 8 insertions, 6 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 60e38d97f4..2008e5f01f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -555,11 +555,13 @@ let vernac_end_modtype (loc,id) = Dumpglob.dump_modref loc mp "modtype"; if_verbose message ("Module Type "^ string_of_id id ^" is defined") -let vernac_include = function +let vernac_include is_self = function | CIMTE mty_ast -> - Declaremods.declare_include Modintern.interp_modtype mty_ast false + Declaremods.declare_include + Modintern.interp_modtype mty_ast false is_self | CIME mexpr_ast -> - Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true + Declaremods.declare_include + Modintern.interp_modexpr mexpr_ast true is_self (**********************) (* Gallina extensions *) @@ -1331,8 +1333,8 @@ let interp c = match c with vernac_define_module export lid bl mtyo mexpro | VernacDeclareModuleType (lid,bl,mtyo) -> vernac_declare_module_type lid bl mtyo - | VernacInclude (in_ast) -> - vernac_include in_ast + | VernacInclude (is_self,in_ast) -> + vernac_include is_self in_ast (* Gallina extensions *) | VernacBeginSection lid -> vernac_begin_section lid diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 8a70e76260..366308bfa6 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -264,7 +264,7 @@ type vernac_expr = module_binder list * (module_type_ast * bool) option * module_ast option | VernacDeclareModuleType of lident * module_binder list * module_type_ast option - | VernacInclude of include_ast + | VernacInclude of bool * include_ast (* Solving *) |