diff options
| -rw-r--r-- | library/declaremods.ml | 30 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 13 |
2 files changed, 37 insertions, 6 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 0ed617a0b..1644b7a7c 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -909,6 +909,36 @@ let declare_one_include interp_struct me_ast is_mod is_self = in let subst = compute_subst mbids mb_mp.mod_type in ([],mp_self,subst_objects subst objects)) + | MSEapply(fexpr, MSEident p) as mexpr -> + let _,mb_mp,mp_l = if is_mod then + get_objs_module_application env mexpr + else + let o,mtb_mp,mp_l = get_objs_modtype_application env mexpr in + o,Modops.module_body_of_type mtb_mp.typ_mp mtb_mp,mp_l in + let mb_mp = + List.fold_left (fun mb _ -> + match mb.mod_type with + | SEBfunctor(_,_,str) -> {mb with mod_type = str} + | _ -> error ("Application of a functor with too much arguments.")) + mb_mp mp_l in + (match objs with + |([],_,_) -> objs + |(mbids,mp_self,objects) -> + let mb = Global.pack_module() in + let rec compute_subst mbids sign = + match mbids with + [] -> empty_subst + | mbid::mbids -> + let farg_id, farg_b, fbody_b = + Modops.destr_functor env sign in + let subst=compute_subst mbids fbody_b in + let mp_delta = + Modops.complete_inline_delta_resolver env mb.mod_mp + farg_id farg_b mb.mod_delta in + join (map_mbid mbid mb.mod_mp mp_delta) subst + in + let subst = compute_subst mbids mb_mp.mod_type in + ([],mp_self,subst_objects subst objects)) | _ -> objs in diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index c473fc6d2..a37e3e5df 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -311,9 +311,9 @@ let vernac_definition (local,boxed,k) (loc,id as lid) def hook = Dumpglob.dump_definition lid false "def"; (match def with | ProveBody (bl,t) -> (* local binders, typ *) - let hook _ _ = () in - start_proof_and_print (local,DefinitionBody Definition) - [Some lid, (bl,t)] hook + let hook _ _ = () in + start_proof_and_print (local,DefinitionBody Definition) + [Some lid, (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None @@ -514,11 +514,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = match mty_ast_l with | [] -> check_no_pending_proofs (); - let binders_ast,argsexport = - List.fold_right + let binders_ast,argsexport = + List.fold_right (fun (export,idl,ty) (args,argsexport) -> - (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast + (idl,ty)::args, (List.map (fun (_,i) -> export,i)idl)@argsexport) binders_ast ([],[]) in + let mp = Declaremods.start_modtype Modintern.interp_modtype id binders_ast mty_sign in Dumpglob.dump_moddef loc mp "modtype"; |