* 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

5 files changed, 15 insertions, 11 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 917accce9d..7e834270d8 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -284,7 +284,7 @@ let with_magic_number_check f a =
 let mk_library md f get_table digest = {
   library_name = md.md_name;
   library_filename = f;
-  library_compiled = Safe_typing.LightenLibrary.load false get_table md.md_compiled;
+  library_compiled = Safe_typing.LightenLibrary.load true get_table md.md_compiled;
   library_deps = md.md_deps;
   library_digest = digest }
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 1b92aaf339..1cb79cb7ab 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -29,7 +29,7 @@ let term_quality = ref false
 
 let xml_export = ref false
 
-let dont_load_proofs = ref false
+let load_proofs = ref false
 
 let raw_print = ref false
 
diff --git a/lib/flags.mli b/lib/flags.mli
index 1d18b4c516..7c46686778 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -21,7 +21,7 @@ val term_quality : bool ref
 
 val xml_export : bool ref
 
-val dont_load_proofs : bool ref
+val load_proofs : bool ref
 
 val raw_print : bool ref
 
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
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index b424006624..e55d6be823 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -232,7 +232,7 @@ let parse_args arglist =
     | "-compile-verbose" :: f :: rem -> add_compile true f;  if not !glob_opt then Dumpglob.dump_to_dotglob (); parse rem
     | "-compile-verbose" :: []       -> usage ()
 
-    | "-dont-load-proofs" :: rem -> Flags.dont_load_proofs := true; parse rem
+    | "-load-proofs" :: rem -> Flags.load_proofs := true; parse rem
 
     | "-beautify" :: rem -> make_beautify true; parse rem