From 59875f3e9e3898402fa5f4504c692dd86b44eba1 Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 27 Aug 2010 09:17:05 +0000
Subject: * library/Library: Remove lighten_library definition.

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

diff --git a/library/library.ml b/library/library.ml
index ff0da8c740..7c734e3a95 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -387,9 +387,6 @@ let try_locate_qualified_library (loc,qid) =
 (************************************************************************)
 (* Internalise libraries *)
 
-let lighten_library m =
-  if !Flags.dont_load_proofs then lighten_library m else m
-
 let mk_library md digest = {
   library_name = md.md_name;
   library_compiled = lighten_library md.md_compiled;
-- 
cgit v1.2.3