Modops: the strengthening functions can work without any env argument

 The env was used for a particular case of Cbytegen.compile_constant_body,
 but we can actually guess that it will answer a particular BCallias con.

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

4 files changed, 35 insertions, 49 deletions

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index d35dfaff1..285039eae 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -278,7 +278,7 @@ and check_structure_field env mp lab res = function
 and check_modexpr env mse mp_mse res = match mse with
   | SEBident mp ->
       let mb = lookup_module mp env in
-      	(subst_and_strengthen mb mp_mse env).mod_type
+      (subst_and_strengthen mb mp_mse).mod_type
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb ;
       let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
@@ -291,7 +291,7 @@ and check_modexpr env mse mp_mse res = match mse with
 	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
 	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
 	check_subtypes env mtb farg_b;
 	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
   | SEBwith(mte, with_decl) ->
@@ -319,7 +319,7 @@ and check_modtype env mse mp_mse res = match mse with
 	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
 	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
 	check_subtypes env mtb farg_b;
 	subst_struct_expr (map_mbid farg_id mp) fbody_b
   | SEBwith(mte, with_decl) ->
diff --git a/checker/modops.ml b/checker/modops.ml
index 4e2bbc210..2dc5d062c 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -94,24 +94,22 @@ and add_module mb env =
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-let strengthen_const env mp_from l cb resolver = 
+let strengthen_const mp_from l cb resolver =
   match cb.const_body with
     | Def _ -> cb
     | _ ->
       let con = make_con mp_from empty_dirpath l in
       (* let con =  constant_of_delta resolver con in*)
-      let const = Const con in
-      let def = Def (Declarations.from_val const) in
-      { cb with const_body = def }
+      { cb with const_body = Def (Declarations.from_val (Const con)) }
 
-let rec strengthen_mod env mp_from mp_to mb = 
+let rec strengthen_mod mp_from mp_to mb =
   if Declarations.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
+	   strengthen_sig mp_from sign mp_to mb.mod_delta in
 	   { mb with
 	       mod_expr = Some (SEBident mp_to);
 	       mod_type = SEBstruct(sign_out);
@@ -123,44 +121,33 @@ let rec strengthen_mod env mp_from mp_to mb =
      | 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
+	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
-	  resolve_out
-	  (*add_delta_resolver resolve_out mb.mod_delta*),
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out (*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
+	resolve_out,item::rest'
+
+let strengthen mtb mp =
     match mtb.typ_expr with
       | 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 = resolve_out(*add_delta_resolver mtb.typ_delta
@@ -168,15 +155,14 @@ let strengthen env mtb mp =
       | SEBfunctor _ -> mtb
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-let subst_and_strengthen mb mp env =
-  strengthen_mod env mb.mod_mp mp 
-    (subst_module (map_mp mb.mod_mp mp) mb)
+let subst_and_strengthen mb mp =
+  strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
 
 
-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;
diff --git a/checker/modops.mli b/checker/modops.mli
index b0bc0ee7f..5ed7b0ce2 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -20,7 +20,7 @@ open Environ
 (* make the envirconment entry out of type *)
 val module_body_of_type : module_path -> module_type_body -> module_body
 
-val module_type_of_module : env -> module_path option -> module_body ->
+val module_type_of_module : module_path option -> module_body ->
   module_type_body
 
 val destr_functor :
@@ -31,9 +31,9 @@ val add_signature : module_path -> structure_body -> delta_resolver -> env -> en
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
-val strengthen : env -> module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> module_path -> module_type_body
 
-val subst_and_strengthen : module_body -> module_path -> env -> module_body 
+val subst_and_strengthen : module_body -> module_path -> module_body
 
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 50d27ce2c..0603300ba 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -285,8 +285,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
    | _ -> error ()
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
-  let mty1 = module_type_of_module env None msb1 in
-  let mty2 =  module_type_of_module env None msb2 in
+  let mty1 = module_type_of_module None msb1 in
+  let mty2 = module_type_of_module None msb2 in
     check_modtypes env mty1 mty2 subst1 subst2 false;
  
 
@@ -368,7 +368,7 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   (*if sup<>super then*)
-  let env = add_module 
-    (module_body_of_type sup.typ_mp sup) env in
-    check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst 
-      (map_mp super.typ_mp sup.typ_mp) false 
+  let env = add_module (module_body_of_type sup.typ_mp sup) env
+  in
+  check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
+      (map_mp super.typ_mp sup.typ_mp) false