Memory optimisation for modules and constrs substitutions.

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

1 files changed, 15 insertions, 19 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 3e89112ae..8770afe13 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -266,26 +266,22 @@ and constants_of_modtype env mp modtype =
 (* returns a resolver for kn that maps mbid to mp *)
 let resolver_of_environment mbid modtype mp env =
  let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve = 
-   List.map
-     (fun (con,expecteddef) ->
-	let con' = replace_mp_in_con (MPbound mbid) mp con in
-	let constr =
-	  try
-	    if expecteddef.Declarations.const_inline then
-              let constant = lookup_constant con' env in
-		if constant.Declarations.const_opaque then
-		  None
-		else
-		  option_map Declarations.force
-		    constant.Declarations.const_body
-	    else
-              None
-	  with Not_found -> error_no_such_label (con_label con')
-	in
-	  con,constr
-     ) constants
+ let rec make_resolve = function
+   | [] -> []
+   | (con,expecteddef)::r ->
+       let con' = replace_mp_in_con (MPbound mbid) mp con in
+	 try
+	   if expecteddef.Declarations.const_inline then
+	     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
+		 (con,constr)::(make_resolve r)
+	     else make_resolve r
+	   else make_resolve r
+	 with Not_found -> error_no_such_label (con_label con')
  in
+ let resolve = make_resolve constants in
    Mod_subst.make_resolver resolve
 
 let strengthen_const env mp l cb =