Modops.destr_functor without useless env

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

1 files changed, 6 insertions, 9 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