Now "Include Self <expr>" 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

1 files changed, 30 insertions, 0 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