Modops.destr_functor without useless env

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16629 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 63 insertions, 59 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index b24deb0dc..f7f3c2b77 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -44,13 +44,10 @@ let rec list_split_assoc ((k,m) as km) rev_before = function
   | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) -> rev_before,b,after
   | h::tail -> list_split_assoc km (h::rev_before) tail
 
-let discr_resolver env mtb =
-     match mtb.typ_expr with
-	SEBstruct _ -> 
-	  mtb.typ_delta
-      | _ -> (*case mp is a functor *)
-	  empty_delta_resolver
-	
+let discr_resolver mtb = match mtb.typ_expr with
+  | SEBstruct _ -> mtb.typ_delta
+  | _ -> empty_delta_resolver (* when mp is a functor *)
+
 let rec rebuild_mp mp l =
   match l with
       []-> mp
@@ -272,14 +269,14 @@ and translate_module env mp inl me =
 
 and translate_apply env inl ftrans mexpr mkalg =
   let sign,alg,resolver,cst1 = ftrans in
-  let farg_id, farg_b, fbody_b = destr_functor env sign in
+  let farg_id, farg_b, fbody_b = destr_functor sign in
   let mp1 =
     try path_of_mexpr mexpr
     with Not_path -> error_application_to_not_path mexpr
   in
   let mtb = module_type_of_module None (lookup_module mp1 env) in
   let cst2 = check_subtypes env mtb farg_b in
-  let mp_delta = discr_resolver env mtb in
+  let mp_delta = discr_resolver mtb in
   let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
   let subst = map_mbid farg_id mp1 mp_delta
   in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 6c46ad510..3b789016b 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -119,7 +119,7 @@ let error_no_such_label_sub l l1 =
 
 (************************)
 
-let destr_functor env mtb =
+let destr_functor mtb =
   match mtb with
   | SEBfunctor (arg_id,arg_t,body_t) ->
       	    (arg_id,arg_t,body_t)
@@ -299,17 +299,20 @@ let rec strengthen_mod mp_from mp_to mb =
     match mb.mod_type with
      | 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
-	       (add_delta_resolver mb.mod_delta resolve_out);
-	       mod_retroknowledge = mb.mod_retroknowledge}
+           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
+	     (add_delta_resolver mb.mod_delta resolve_out);
+	   mod_retroknowledge = mb.mod_retroknowledge }
      | SEBfunctor _ -> mb
-     | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+     | _ ->
+       anomaly ~label:"Modops"
+         (Pp.str "the evaluation of the structure failed ")
 
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
@@ -340,13 +343,16 @@ let strengthen mtb mp =
     match mtb.typ_expr with
       | SEBstruct (sign) ->
 	  let resolve_out,sign_out =
-	    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)}
+	    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 ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+      | _ ->
+        anomaly ~label:"Modops"
+          (Pp.str "the evaluation of the structure failed ")
 
 let module_type_of_module mp mb =
   match mp with
@@ -386,32 +392,32 @@ let inline_delta_resolver env inl mp mbid mtb delta =
   in
   make_inline delta constants
 
-let rec strengthen_and_subst_mod
-    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
-	   if mb_is_an_alias then 
-	     subst_module subst 
-	       (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb 
-	   else
-	     let resolver,new_sig = 
-	       strengthen_and_subst_struct str subst
-		 mp_from mp_from mp_to false false mb.mod_delta 
-	     in
-	       {mb with 
-		  mod_mp = mp_to;
-		  mod_expr = Some (SEBident mp_from);
-		  mod_type = SEBstruct(new_sig);
-		  mod_delta = add_mp_delta_resolver mp_to mp_from resolver}
-       | SEBfunctor(arg_id,arg_b,body) ->
-	   let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
-	   subst_module subst 
-	     (fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb  
-	
-       | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-	   
-and strengthen_and_subst_struct 
+let rec strengthen_and_subst_mod 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
+      if mb_is_an_alias then
+	subst_module subst
+	  (fun resolver subst-> subst_dom_delta_resolver subst resolver) mb
+      else
+	let resolver,new_sig =
+	  strengthen_and_subst_struct str subst
+	    mp_from mp_from mp_to false false mb.mod_delta
+	in
+	{mb with
+	  mod_mp = mp_to;
+	  mod_expr = Some (SEBident mp_from);
+	  mod_type = SEBstruct(new_sig);
+	  mod_delta = add_mp_delta_resolver mp_to mp_from resolver}
+    | SEBfunctor(arg_id,arg_b,body) ->
+      let subst = add_mp mb.mod_mp mp_to empty_delta_resolver subst in
+      subst_module subst
+	(fun resolver subst-> subst_dom_codom_delta_resolver subst resolver) mb
+    | _ ->
+      anomaly ~label:"Modops"
+        (Pp.str "the evaluation of the structure failed ")
+
+and strengthen_and_subst_struct
     str subst mp_alias mp_from mp_to alias incl resolver =
   match str with
     | [] -> empty_delta_resolver,[]
@@ -485,10 +491,11 @@ and strengthen_and_subst_struct
 	let mty = subst_modtype subst' 
 	  (fun resolver subst -> subst_dom_codom_delta_resolver subst' resolver) mty in
 	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'
-    
+	    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 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
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 66aadd124..c4d8ab349 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -23,7 +23,7 @@ val module_type_of_module : module_path option -> module_body ->
   module_type_body
 
 val destr_functor :
-  env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body
+  struct_expr_body -> MBId.t * module_type_body * struct_expr_body
 
 val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 0a5b61656..468f7229b 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -388,7 +388,7 @@ let rec compute_subst env mbids sign mp_l inl =
     | _,[] -> mbids,empty_subst
     | [],r -> error "Application of a functor with too few arguments."
     | mbid::mbids,mp::mp_l ->
-	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
 	let mb = Environ.lookup_module mp env in
 	let mbid_left,subst = compute_subst env mbids fbody_b mp_l inl in
 	let resolver = match discr_resolver mb with
@@ -791,7 +791,7 @@ let rec include_subst env mp reso mbids sign inline =
   match mbids with
     | [] -> empty_subst
     | mbid::mbids ->
-	let farg_id, farg_b, fbody_b = Modops.destr_functor env sign in
+	let farg_id, farg_b, fbody_b = Modops.destr_functor sign in
 	let subst = include_subst env mp reso mbids fbody_b inline in
 	let mp_delta =
 	  Modops.inline_delta_resolver env inline mp farg_id farg_b reso