Added a lazy evaluation of the composition of module substitutions. It improves speed of functor application and size of .vo which use them.

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

1 files changed, 5 insertions, 5 deletions

diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 930d9aa7d..640aecb98 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -693,7 +693,7 @@ let occur_mbid uid = occur_uid (MBI uid)
 
 type 'a lazy_subst =
   | LSval of 'a
-  | LSlazy of substitution * 'a
+  | LSlazy of substitution list * 'a
 
 type 'a substituted = 'a lazy_subst ref
 
@@ -703,14 +703,14 @@ let force fsubst r =
   match !r with
   | LSval a -> a
   | LSlazy(s,a) ->
-      let a' = fsubst s a in
+      let subst = List.fold_left join empty_subst (List.rev s) in
+      let a' = fsubst subst a in
       r := LSval a';
       a'
 
 let subst_substituted s r =
   match !r with
-    | LSval a -> ref (LSlazy(s,a))
+    | LSval a -> ref (LSlazy([s],a))
     | LSlazy(s',a) ->
-	let s'' = join s' s in
-	  ref (LSlazy(s'',a))
+	  ref (LSlazy(s::s',a))