From 10cd48958553133115d0d95b1c9bdc0810aee576 Mon Sep 17 00:00:00 2001 From: soubiran Date: Wed, 18 Nov 2009 15:12:05 +0000 Subject: Now "Include Self " handles partially applied functors, cf for example NZAddPropFunct in NZAdd.v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12535 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/declaremods.ml | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) (limited to 'library/declaremods.ml') 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 -- cgit v1.2.3