Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 210 insertions, 194 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index f0d579a4..0c2c6bd7 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -1,14 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+(* Inlining and more liberal use of modules and module types by Claudio
+   Sacerdoti, Nov 2004 *)
+(* New structure-based model of modules and miscellaneous bug fixes by
+   Élie Soubiran, from Feb 2008 *)
+
+(* This file provides with various operations on modules and module types *)
 
-(*i*)
 open Util
 open Pp
 open Names
@@ -18,80 +24,103 @@ open Declarations
 open Environ
 open Entries
 open Mod_subst
-(*i*)
-
-
-
-let error_existing_label l = 
-  error ("The label "^string_of_label l^" is already declared.")
-
-let error_declaration_not_path _ = error "Declaration is not a path."
-
-let error_application_to_not_path _ = error "Application to not path."
-
-let error_not_a_functor _ = error "Application of not a functor."
-
-let error_incompatible_modtypes _ _ = error "Incompatible module types."
-
-let error_not_equal _ _ = error "Non equal modules."
 
-let error_not_match l _ = error ("Signature components for label "^string_of_label l^" do not match.")
-
-let error_no_such_label l = error ("No such label "^string_of_label l^".")
-
-let error_incompatible_labels l l' = 
-  error ("Opening and closing labels are not the same: "
-	 ^string_of_label l^" <> "^string_of_label l'^" !")
-
-let error_result_must_be_signature () = 
-  error "The result module type must be a signature."
+type signature_mismatch_error =
+  | InductiveFieldExpected of mutual_inductive_body
+  | DefinitionFieldExpected
+  | ModuleFieldExpected
+  | ModuleTypeFieldExpected
+  | NotConvertibleInductiveField of identifier
+  | NotConvertibleConstructorField of identifier
+  | NotConvertibleBodyField
+  | NotConvertibleTypeField
+  | NotSameConstructorNamesField
+  | NotSameInductiveNameInBlockField
+  | FiniteInductiveFieldExpected of bool
+  | InductiveNumbersFieldExpected of int
+  | InductiveParamsNumberField of int
+  | RecordFieldExpected of bool
+  | RecordProjectionsExpected of name list
+  | NotEqualInductiveAliases
+  | NoTypeConstraintExpected
+
+type module_typing_error =
+  | SignatureMismatch of label * structure_field_body * signature_mismatch_error
+  | LabelAlreadyDeclared of label
+  | ApplicationToNotPath of module_struct_entry
+  | NotAFunctor of struct_expr_body
+  | IncompatibleModuleTypes of module_type_body * module_type_body
+  | NotEqualModulePaths of module_path * module_path
+  | NoSuchLabel of label
+  | IncompatibleLabels of label * label
+  | SignatureExpected of struct_expr_body
+  | NoModuleToEnd
+  | NoModuleTypeToEnd
+  | NotAModule of string
+  | NotAModuleType of string
+  | NotAConstant of label
+  | IncorrectWithConstraint of label
+  | GenerativeModuleExpected of label
+  | NonEmptyLocalContect of label option
+  | LabelMissing of label * string
+
+exception ModuleTypingError of module_typing_error
+
+let error_existing_label l =
+  raise (ModuleTypingError (LabelAlreadyDeclared l))
+
+let error_application_to_not_path mexpr =
+  raise (ModuleTypingError (ApplicationToNotPath mexpr))
+
+let error_not_a_functor mtb =
+  raise (ModuleTypingError (NotAFunctor mtb))
+
+let error_incompatible_modtypes mexpr1 mexpr2 =
+  raise (ModuleTypingError (IncompatibleModuleTypes (mexpr1,mexpr2)))
+
+let error_not_equal_modpaths mp1 mp2 =
+  raise (ModuleTypingError (NotEqualModulePaths (mp1,mp2)))
+
+let error_signature_mismatch l spec why =
+  raise (ModuleTypingError (SignatureMismatch (l,spec,why)))
+
+let error_no_such_label l =
+  raise (ModuleTypingError (NoSuchLabel l))
+
+let error_incompatible_labels l l' =
+  raise (ModuleTypingError (IncompatibleLabels (l,l')))
 
 let error_signature_expected mtb =
-  error "Signature expected."
+  raise (ModuleTypingError (SignatureExpected mtb))
 
-let error_no_module_to_end _ = 
-  error "No open module to end."
+let error_no_module_to_end _ =
+  raise (ModuleTypingError NoModuleToEnd)
 
 let error_no_modtype_to_end _ =
-  error "No open module type to end."
-
-let error_not_a_modtype_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module type."))
-
-let error_not_a_module_loc loc s = 
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module."))
+  raise (ModuleTypingError NoModuleTypeToEnd)
 
-let error_not_a_module_or_modtype_loc loc s =
-  user_err_loc (loc,"",str ("\""^s^"\" is not a module or module type."))
+let error_not_a_modtype s =
+  raise (ModuleTypingError (NotAModuleType s))
 
-let error_not_a_module s = error_not_a_module_loc dummy_loc s
+let error_not_a_module s =
+  raise (ModuleTypingError (NotAModule s))
 
-let error_not_a_constant l = 
-  error ("\""^(string_of_label l)^"\" is not a constant.")
+let error_not_a_constant l =
+  raise (ModuleTypingError (NotAConstant l))
 
-let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(string_of_label l)^"\".")
+let error_incorrect_with_constraint l =
+  raise (ModuleTypingError (IncorrectWithConstraint l))
 
-let error_a_generative_module_expected l =
-  error ("The module " ^ string_of_label l ^ " is not generative. Only " ^
-         "component of generative modules can be changed using the \"with\" " ^
-         "construct.")
-
-let error_local_context lo = 
-  match lo with
-      None -> 
-	error ("The local context is not empty.")
-    | (Some l) ->
-	error ("The local context of the component "^
-	       (string_of_label l)^" is not empty.")
+let error_generative_module_expected l =
+  raise (ModuleTypingError (GenerativeModuleExpected l))
 
+let error_non_empty_local_context lo =
+  raise (ModuleTypingError (NonEmptyLocalContect lo))
 
 let error_no_such_label_sub l l1 =
-  error ("The field "^(string_of_label l)^" is missing in "^l1^".")
-
-let error_with_in_module _ = error "The syntax \"with\" is not allowed for modules."
+  raise (ModuleTypingError (LabelMissing (l,l1)))
 
-let error_application_to_module_type _ = error "Module application to a module type."
+(************************)
 
 let destr_functor env mtb =
   match mtb with
@@ -116,9 +145,9 @@ let check_modpath_equiv env mp1 mp2 =
   if mp1=mp2 then () else
     let mb1=lookup_module  mp1 env in
     let mb2=lookup_module mp2 env in
-      if (delta_of_mp mb1.mod_delta mp1)=(delta_of_mp mb2.mod_delta mp2)
+      if (mp_of_delta mb1.mod_delta mp1)=(mp_of_delta mb2.mod_delta mp2)
       then ()
-      else error_not_equal mp1 mp2
+      else error_not_equal_modpaths mp1 mp2
 	
 let rec subst_with_body sub = function
   | With_module_body(id,mp) ->
@@ -235,18 +264,13 @@ let add_retroknowledge mp =
 let rec add_signature mp sign resolver env = 
   let add_one env (l,elem) =
     let kn = make_kn mp empty_dirpath l in
-    let con = constant_of_kn kn in
-    let mind = mind_of_kn kn in
-      match elem with
-	| SFBconst cb -> 
-	    let con =  constant_of_delta resolver con in
-	      Environ.add_constant con cb env
-	| SFBmind mib -> 
-	    let mind =  mind_of_delta resolver mind in
-	    Environ.add_mind mind mib env
-	| SFBmodule mb -> add_module mb env
-	      (* adds components as well *)
-	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
+    match elem with
+      | SFBconst cb ->
+	Environ.add_constant (constant_of_delta_kn resolver kn) cb env
+      | SFBmind mib ->
+	Environ.add_mind (mind_of_delta_kn resolver kn) mib env
+      | SFBmodule mb -> add_module mb env (* adds components as well *)
+      | SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
   in
     List.fold_left add_one env sign
 
@@ -260,100 +284,83 @@ and add_module mb env =
       | SEBfunctor _ -> env
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-let strengthen_const env mp_from l cb resolver = 
-  match cb.const_opaque, cb.const_body with
-  | false, Some _ -> cb
-  | true, Some _ 
-  | _, None ->
-      let con = make_con mp_from empty_dirpath l in
-      let con =  constant_of_delta resolver con in
-      let const = mkConst con in 
-      let const_subs = Some (Declarations.from_val const) in
-	{cb with 
-	   const_body = const_subs;
-	   const_opaque = false;
-	   const_body_code = Cemitcodes.from_val
-            (compile_constant_body env const_subs false false)
-	}
-	  
-
-let rec strengthen_mod env mp_from mp_to mb = 
+let strengthen_const mp_from l cb resolver =
+  match cb.const_body with
+    | Def _ -> cb
+    | _ ->
+      let kn = make_kn mp_from empty_dirpath l in
+      let con = constant_of_delta_kn resolver kn in
+      { cb with
+	const_body = Def (Declarations.from_val (mkConst con));
+	const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con)
+      }
+
+let rec strengthen_mod mp_from mp_to mb =
   if mp_in_delta mb.mod_mp mb.mod_delta then
-    mb 
+    mb
   else
     match mb.mod_type with
-     | SEBstruct (sign) -> 
-	 let resolve_out,sign_out = 
-	   strengthen_sig env mp_from sign mp_to mb.mod_delta in
+     | SEBstruct (sign) ->
+	 let resolve_out,sign_out =
+	   strengthen_sig mp_from sign mp_to mb.mod_delta in
 	   { mb with
 	       mod_expr = Some (SEBident mp_to);
 	       mod_type = SEBstruct(sign_out);
 	       mod_type_alg = mb.mod_type_alg;
 	       mod_constraints = mb.mod_constraints;
-	       mod_delta = add_mp_delta_resolver mp_from mp_to 
+	       mod_delta = add_mp_delta_resolver mp_from mp_to
 	       (add_delta_resolver mb.mod_delta resolve_out);
 	       mod_retroknowledge = mb.mod_retroknowledge}
      | SEBfunctor _ -> mb
      | _ -> anomaly "Modops:the evaluation of the structure failed "
-	 
-and strengthen_sig env mp_from sign mp_to resolver =
+
+and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = 
-	  l,SFBconst (strengthen_const env mp_from l cb resolver) in
-	let resolve_out,rest' =
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item'::rest'
+	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = 
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in 
-	let mb_out = 
-	  strengthen_mod env mp_from' mp_to' mb in
+	let mp_to' = MPdot(mp_to,l) in
+	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
-	let env' = add_module mb_out env in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  add_delta_resolver resolve_out mb.mod_delta,
-	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
-	let env' = add_modtype 
-	  (MPdot(mp_from,l)) mty env
-	in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
-    
-let strengthen env mtb mp = 
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	add_delta_resolver resolve_out mb.mod_delta, item':: rest'
+    | (l,SFBmodtype mty as item) :: rest ->
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item::rest'
+
+let strengthen mtb mp =
   if mp_in_delta mtb.typ_mp mtb.typ_delta then
     (* in this case mtb has already been strengthened*)
-    mtb 
+    mtb
   else
     match mtb.typ_expr with
-      | SEBstruct (sign) -> 
+      | SEBstruct (sign) ->
 	  let resolve_out,sign_out =
-	    strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in
+	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
 	    {mtb with
 	       typ_expr = SEBstruct(sign_out);
 	       typ_delta = add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)}
       | SEBfunctor _ -> mtb
       | _ -> anomaly "Modops:the evaluation of the structure failed "
-	  
-let module_type_of_module env mp mb =
+
+let module_type_of_module mp mb =
   match mp with
       Some mp ->
-	strengthen env {
+	strengthen {
 	  typ_mp = mp;
 	  typ_expr = mb.mod_type;
 	  typ_expr_alg = None;
 	  typ_constraints = mb.mod_constraints;
 	  typ_delta = mb.mod_delta} mp
-	  
+
     | None ->
 	{typ_mp = mb.mod_mp;
 	 typ_expr = mb.mod_type;
@@ -361,34 +368,29 @@ let module_type_of_module env mp mb =
 	 typ_constraints = mb.mod_constraints;
 	 typ_delta = mb.mod_delta}
 
-let complete_inline_delta_resolver env mp mbid mtb delta =
-  let constants = inline_of_delta mtb.typ_delta in
+let inline_delta_resolver env inl mp mbid mtb delta =
+  let constants = inline_of_delta inl mtb.typ_delta in
   let rec make_inline delta = function
     | [] -> delta
-    | kn::r -> 
+    | (lev,kn)::r ->
 	let kn = replace_mp_in_kn (MPbound mbid) mp kn in
-	let con = constant_of_kn kn in
-	let con' = constant_of_delta delta con in
-	  try
-	    let constant = lookup_constant con' env in
-	      if (not constant.Declarations.const_opaque) then
-		let constr = Option.map Declarations.force 
-		  constant.Declarations.const_body in
-		  if constr = None then 
-		    (make_inline delta r)
-		  else
-		    add_inline_constr_delta_resolver con (Option.get constr)
-		      (make_inline delta r)
-	      else
-		(make_inline delta r)
-	  with 
-	      Not_found -> error_no_such_label_sub (con_label con) 
-		(string_of_mp (con_modpath con))
+	let con = constant_of_delta_kn delta kn in
+	try
+	  let constant = lookup_constant con env in
+	  let l = make_inline delta r in
+	  match constant.const_body with
+	    | Undef _ | OpaqueDef _ -> l
+	    | Def body ->
+	      let constr = Declarations.force body in
+	      add_inline_delta_resolver kn (lev, Some constr) l
+	with Not_found ->
+	  error_no_such_label_sub (con_label con)
+	    (string_of_mp (con_modpath con))
   in
-    make_inline delta constants
+  make_inline delta constants
 
 let rec strengthen_and_subst_mod
-    mb subst env mp_from mp_to env resolver =
+    mb subst mp_from mp_to resolver =
      match mb.mod_type with
 	 SEBstruct(str) ->
 	   let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
@@ -397,7 +399,7 @@ let rec strengthen_and_subst_mod
 	       (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb 
 	   else
 	     let resolver,new_sig = 
-	       strengthen_and_subst_struct str subst env
+	       strengthen_and_subst_struct str subst
 		 mp_from mp_from mp_to false false mb.mod_delta 
 	     in
 	       {mb with 
@@ -413,42 +415,48 @@ let rec strengthen_and_subst_mod
        | _ -> anomaly "Modops:the evaluation of the structure failed "
 	   
 and strengthen_and_subst_struct 
-    str subst env mp_alias mp_from mp_to alias incl resolver =
+    str subst mp_alias mp_from mp_to alias incl resolver =
   match str with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = if alias then
+	let item' = if alias then 
+	  (* case alias no strengthening needed*)
 	  l,SFBconst (subst_const_body subst cb) 
 	else 
-	  l,SFBconst (strengthen_const env mp_from l 
+	  l,SFBconst (strengthen_const mp_from l
 			(subst_const_body subst cb) resolver)
 	in
-	let con = make_con mp_from empty_dirpath l in
 	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst env 
+	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if incl then
-	    let old_name = constant_of_delta resolver con in
-	    (add_constant_delta_resolver
-	      (constant_of_kn_equiv (make_kn mp_to empty_dirpath l)
-		 (canonical_con old_name)) 
-	      resolve_out),
-	item'::rest'
-	  else
-	    resolve_out,item'::rest'
+	if incl then
+	    (* If we are performing an inclusion we need to add
+	       the fact that the constant mp_to.l is \Delta-equivalent
+	       to resolver(mp_from.l) *)
+	  let kn_from = make_kn mp_from empty_dirpath l in
+	  let kn_to = make_kn mp_to empty_dirpath l in
+	  let old_name = kn_of_delta resolver kn_from in
+	  (add_kn_delta_resolver kn_to old_name resolve_out),
+	  item'::rest'
+	else
+	    (*In this case the fact that the constant mp_to.l is 
+	      \Delta-equivalent to resolver(mp_from.l) is already known
+	       because resolve_out contains mp_to maps to resolver(mp_from)*)
+	  resolve_out,item'::rest'
     | (l,SFBmind mib) :: rest ->
+	(*Same as constant*)
 	let item' = l,SFBmind (subst_mind subst mib) in
-	let mind = make_mind mp_from empty_dirpath l in
 	let resolve_out,rest' =
-	  strengthen_and_subst_struct rest subst env 
+	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if incl then
-	    let old_name =  mind_of_delta resolver mind in 
-	    (add_mind_delta_resolver
-	      (mind_of_kn_equiv (make_kn mp_to empty_dirpath l) (canonical_mind old_name)) resolve_out),
-	item'::rest'
-	  else
-	    resolve_out,item'::rest'
+	if incl then
+	  let kn_from = make_kn mp_from empty_dirpath l in
+	  let kn_to = make_kn mp_to empty_dirpath l in
+	  let old_name = kn_of_delta resolver kn_from in
+	  (add_kn_delta_resolver kn_to old_name resolve_out),
+	  item'::rest'
+	else
+	  resolve_out,item'::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
 	let mp_to' = MPdot(mp_to,l) in
@@ -457,15 +465,20 @@ and strengthen_and_subst_struct
 	  (fun resolver subst -> subst_dom_delta_resolver subst resolver) mb 
 	else
 	  strengthen_and_subst_mod
-	    mb subst env mp_from' mp_to' env resolver
+	    mb subst mp_from' mp_to' resolver
 	in
 	let item' = l,SFBmodule (mb_out) in
-	let env' = add_module mb_out env in
-	let resolve_out,rest' = 
-	  strengthen_and_subst_struct rest subst env' 
+	let resolve_out,rest' =
+	  strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
-	  if  is_functor mb_out.mod_type then (add_mp_delta_resolver 
-	     mp_to' mp_to' resolve_out),item':: rest' else
+	  (* if mb is a functor we should not derive new equivalences
+	     on names, hence we add the fact that the functor can only
+	     be equivalent to itself. If we adopt an applicative
+	     semantic for functor this should be changed.*)
+	  if is_functor mb_out.mod_type then 
+	    (add_mp_delta_resolver 
+	       mp_to' mp_to' resolve_out),item':: rest' 
+	  else
 	    add_delta_resolver resolve_out mb_out.mod_delta,
 	item':: rest'
     | (l,SFBmodtype mty) :: rest -> 
@@ -474,27 +487,30 @@ and strengthen_and_subst_struct
 	let subst' = add_mp mp_from' mp_to' empty_delta_resolver subst in
 	let mty = subst_modtype subst' 
 	  (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
-	let env' = add_modtype mp_from' mty env	in
-	let resolve_out,rest' = strengthen_and_subst_struct rest subst env' 
+	let resolve_out,rest' = strengthen_and_subst_struct rest subst
 	    mp_alias mp_from mp_to alias incl resolver in
 	  (add_mp_delta_resolver 
 	     mp_to' mp_to' resolve_out),(l,SFBmodtype mty)::rest'
     
-let strengthen_and_subst_mb mb mp env include_b =
+
+(* Let P be a module path when we write "Module M:=P." or "Module M. Include P. End M."
+   we need to perform two operations to compute the body of M. The first one is applying
+   the substitution {P <- M} on the type of P and the second one is strenghtening. *)
+let strengthen_and_subst_mb mb mp include_b =
     match mb.mod_type with
 	SEBstruct str ->
 	  let mb_is_an_alias = mp_in_delta mb.mod_mp mb.mod_delta in
-	    (*if mb is an alias then the strengthening is useless 
+	    (*if mb.mod_mp is an alias then the strengthening is useless 
 	      (i.e. it is already done)*)
-	  let mp_alias = delta_of_mp mb.mod_delta mb.mod_mp in
+	  let mp_alias = mp_of_delta mb.mod_delta mb.mod_mp in
 	  let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in
 	  let new_resolver = 
 	    add_mp_delta_resolver mp mp_alias
-	      (subst_dom_delta_resolver subst_resolver mb.mod_delta) in	    
+	      (subst_dom_delta_resolver subst_resolver mb.mod_delta) in
 	  let subst = map_mp mb.mod_mp mp new_resolver in 
 	  let resolver_out,new_sig = 
-	    strengthen_and_subst_struct str subst env
-	     mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta
+	    strengthen_and_subst_struct str subst
+	     mp_alias mb.mod_mp mp mb_is_an_alias include_b mb.mod_delta 
 	  in
 	    {mb with 
 	       mod_mp = mp;
@@ -509,7 +525,7 @@ let strengthen_and_subst_mb mb mp env include_b =
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-let subst_modtype_and_resolver mtb mp env =
+let subst_modtype_and_resolver mtb mp =
   let subst = (map_mp mtb.typ_mp mp empty_delta_resolver) in
   let new_delta = subst_dom_codom_delta_resolver subst mtb.typ_delta in 
   let full_subst = (map_mp mtb.typ_mp mp new_delta) in