Some dead code removal, thanks to Oug analyzer

 In particular, the unused lib/tlm.ml and lib/gset.ml are removed

 In addition, to simplify code, Libobject.record_object returning only the
 ('a->obj) function, which is enough almost all the time.
 Use Libobject.record_object_full if you really need also the (obj->'a).

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

1 files changed, 2 insertions, 7 deletions

diff --git a/library/library.ml b/library/library.ml
index c1673925c..45d5c8f58 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -66,8 +66,6 @@ let add_load_path isroot (phys_path,coq_path) =
 	  load_paths := (phys_path,coq_path,isroot) :: !load_paths;
       | _ -> anomaly ("Two logical paths are associated to "^phys_path)
 
-let physical_paths (dp,lp) = dp
-
 let extend_path_with_dirpath p dir =
   List.fold_left Filename.concat p
     (List.map string_of_id (List.rev (repr_dirpath dir)))
@@ -213,9 +211,6 @@ let library_is_loaded dir =
 let library_is_opened dir =
   List.exists (fun m -> m.library_name = dir) !libraries_imports_list
 
-let library_is_exported dir =
-  List.exists (fun m -> m.library_name = dir) !libraries_exports_list
-
 let loaded_libraries () =
   List.map (fun m -> m.library_name) !libraries_loaded_list
 
@@ -305,7 +300,7 @@ let subst_import (_,o) = o
 let classify_import (_,export as obj) =
   if export then Substitute obj else Dispose
 
-let (in_import, out_import) =
+let in_import =
   declare_object {(default_object "IMPORT LIBRARY") with
        cache_function = cache_import;
        open_function = open_import;
@@ -517,7 +512,7 @@ let discharge_require (_,o) = Some o
 
 (* open_function is never called from here because an Anticipate object *)
 
-let (in_require, out_require) =
+let in_require =
   declare_object {(default_object "REQUIRE") with
        cache_function = cache_require;
        load_function = load_require;