diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernacentries.ml | 14 | ||||
-rw-r--r-- | toplevel/vernacexpr.ml | 1 |
2 files changed, 12 insertions, 3 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index fed36d004..ec60cc52e 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -470,10 +470,17 @@ let vernac_end_modtype id = if_verbose message ("Module Type "^ string_of_id id ^" is defined") - +let vernac_include = function + | CIMTE mty_ast -> + Declaremods.declare_include Modintern.interp_modtype mty_ast false + | CIME mexpr_ast -> + Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true + + + (**********************) (* Gallina extensions *) - + let vernac_record struc binders sort nameopt cfs = let const = match nameopt with | None -> add_prefix "Build_" (snd (snd struc)) @@ -1198,7 +1205,8 @@ let interp c = match c with vernac_define_module export id bl mtyo mexpro | VernacDeclareModuleType ((_,id),bl,mtyo) -> vernac_declare_module_type id bl mtyo - + | VernacInclude (in_ast) -> + vernac_include in_ast (* Gallina extensions *) | VernacBeginSection (_,id) -> vernac_begin_section id diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 3571b121b..cf7fb72c6 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -249,6 +249,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 (* Solving *) |