1 files changed, 51 insertions, 2 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0a18978327..2808973fa6 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -124,6 +124,9 @@ let rec check_modpath_equiv env mp1 mp2 =
 
 
 let rec subst_modtype sub = function
+    (* This is the case in which I am substituting a whole module.
+       For instance "Module M(X). Module N := X. End M". When I apply
+       M to M' I must substitute M' for X in "Module N := X". *)
   | MTBident ln -> MTBident (subst_kn sub ln)
   | MTBfunsig (arg_id, arg_b, body_b) ->
       if occur_mbid arg_id sub then failwith "capture";
@@ -149,16 +152,62 @@ and subst_signature sub sign =
 
 and subst_module sub mb =
   let mtb' = subst_modtype sub mb.msb_modtype in
+  (* This is similar to the previous case. In this case we have
+     a module M in a signature that is knows to be equivalent to a module M'
+     (because the signature is "K with Module M := M'") and we are substituting
+     M' with some M''. *)
   let mpo' = option_smartmap (subst_mp sub) mb.msb_equiv in
     if mtb'==mb.msb_modtype && mpo'==mb.msb_equiv then mb else
       { msb_modtype=mtb'; 
 	msb_equiv=mpo'; 
 	msb_constraints=mb.msb_constraints}
 
-
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
 
+let rec constants_of_specification env mp sign =
+ let aux res (l,elem) =
+  match elem with
+   | SPBconst cb -> (make_con mp empty_dirpath l)::res
+   | SPBmind _ -> res
+   | SPBmodule mb ->
+      (constants_of_modtype env (MPdot (mp,l))
+        (module_body_of_spec mb).mod_type) @ res
+   | SPBmodtype mtb -> res (* ???? *)
+ in
+  List.fold_left aux [] sign
+
+and constants_of_modtype env mp modtype =
+ match scrape_modtype env modtype with
+    MTBident _ -> anomaly "scrape_modtype does not work!"
+  | MTBsig (msid,sign) ->
+     constants_of_specification env mp
+      (subst_signature_msid msid mp sign)
+  | MTBfunsig _ -> []
+
+(* returns a resolver for kn that maps mbid to mp and then delta-expands
+   the obtained constants according to env *)
+let resolver_of_environment mbid modtype mp env =
+ let constants = constants_of_modtype env (MPbound mbid) modtype in
+ let resolve =
+  List.map
+   (fun con ->
+     let con' = replace_mp_in_con (MPbound mbid) mp con in
+     let constr =
+      try
+       let constant = lookup_constant con' env in
+        if constant.Declarations.const_opaque then
+         None
+        else
+         option_app Declarations.force
+          constant.Declarations.const_body
+      with Not_found -> assert false
+     in
+      con,constr
+   ) constants
+ in
+  Mod_subst.make_resolver resolve
+
 (* we assume that the substitution of "mp" into "msid" is already done
 (or unnecessary) *)
 let rec add_signature mp sign env = 
@@ -182,7 +231,6 @@ and add_module mp mb env =
       | MTBident _ -> anomaly "scrape_modtype does not work!"
       | MTBsig (msid,sign) -> 
 	  add_signature mp (subst_signature_msid msid mp sign) env
-
       | MTBfunsig _ -> env
 
 
@@ -247,3 +295,4 @@ and strengthen_sig env msid sign mp = match sign with
 	item::rest'
 
 let strengthen env mtb mp = strengthen_mtb env mp mtb
+