From ec5eb9320d6f88498de6fc1993be8787b75aa17a Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 27 Aug 2010 09:17:09 +0000
Subject: * library/Library: Remove the use of the old-fashioned
 lighten_library.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13376 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/library.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/library.ml b/library/library.ml
index 7c734e3a95..42cad44541 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -389,7 +389,7 @@ let try_locate_qualified_library (loc,qid) =
 
 let mk_library md digest = {
   library_name = md.md_name;
-  library_compiled = lighten_library md.md_compiled;
+  library_compiled = md.md_compiled;
   library_objects = md.md_objects;
   library_deps = md.md_deps;
   library_imports = md.md_imports;
-- 
cgit v1.2.3