From 7350f5de205ea54e277be1d82cc045788182f82e Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 30 May 2007 16:01:18 +0000
Subject: 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
---
 kernel/modops.ml | 34 +++++++++++++++-------------------
 1 file changed, 15 insertions(+), 19 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 3e89112ae3..8770afe131 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 = 
-- 
cgit v1.2.3