From 129a58c5dd2403263b8285f345b3a5e41d480b78 Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 27 Aug 2010 09:17:19 +0000
Subject: * lib/Flags: Replace dont_load_proofs by load_proofs since not
 loading              proofs is now the default behavior of coqtop.

* lib/Coqtop: Update accordingly.

* checker/Check library/Library:
  Pass the right "load_proofs" flag to LightenLibrary.load.

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

(limited to 'library')

diff --git a/library/library.ml b/library/library.ml
index 23b9fdc81a..44aa05b54a 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -387,13 +387,17 @@ let try_locate_qualified_library (loc,qid) =
 (************************************************************************)
 (* Internalise libraries *)
 
-let mk_library md get_table digest = {
-  library_name = md.md_name;
-  library_compiled = LightenLibrary.load false get_table md.md_compiled;
-  library_objects = md.md_objects;
-  library_deps = md.md_deps;
-  library_imports = md.md_imports;
-  library_digest = digest }
+let mk_library md get_table digest = 
+  let md_compiled = 
+    LightenLibrary.load !Flags.load_proofs get_table md.md_compiled
+  in {
+    library_name     = md.md_name;
+    library_compiled = md_compiled;
+    library_objects  = md.md_objects;
+    library_deps     = md.md_deps;
+    library_imports  = md.md_imports;
+    library_digest    = digest 
+  }
 
 let intern_from_file f =
   let ch = System.with_magic_number_check raw_intern_library f in
-- 
cgit v1.2.3