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

13 files changed, 25 insertions, 58 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 0764af4b0..a9c463020 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -78,7 +78,7 @@ let discharge_variable (_,o) = match o with
   | Inr (id,_) -> Some (Inl (variable_constraints id))
   | Inl _ -> Some o
 
-let (inVariable,_) =
+let inVariable =
   declare_object { (default_object "VARIABLE") with
     cache_function = cache_variable;
     discharge_function = discharge_variable;
@@ -145,7 +145,7 @@ let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
 let classify_constant cst = Substitute (dummy_constant cst)
 
-let (inConstant,_) =
+let inConstant =
   declare_object { (default_object "CONSTANT") with
     cache_function = cache_constant;
     load_function = load_constant;
@@ -259,7 +259,7 @@ let dummy_inductive_entry (_,m) = ([],{
   mind_entry_finite = true;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds })
 
-let (inInductive,_) =
+let inInductive =
   declare_object {(default_object "INDUCTIVE") with
     cache_function = cache_inductive;
     load_function = load_inductive;
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 30fa3db65..58b0d6a46 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -262,7 +262,7 @@ let classify_module (_,substobjs) =
   Substitute (None,substobjs)
 
 let (in_module,out_module) =
-  declare_object {(default_object "MODULE") with
+  declare_object_full {(default_object "MODULE") with
     cache_function = cache_module;
     load_function = load_module;
     open_function = open_module;
@@ -289,7 +289,7 @@ let open_keep i ((sp,kn),seg) =
   let dirpath,mp = dir_of_sp sp, mp_of_kn kn in
     open_objects i (dirpath,(mp,empty_dirpath)) seg
 
-let (in_modkeep,_) =
+let in_modkeep =
   declare_object {(default_object "MODULE KEEP OBJECTS") with
     cache_function = cache_keep;
     load_function = load_keep;
@@ -376,7 +376,7 @@ let classify_modtype (_,substobjs,_) =
   Substitute (None,substobjs,[])
 
 
-let (in_modtype,_) =
+let in_modtype =
     declare_object {(default_object "MODULE TYPE") with
       cache_function = cache_modtype;
       open_function = open_modtype;
@@ -649,7 +649,7 @@ let subst_import (subst,(export,mp as obj)) =
     if mp'==mp then obj else
       (export,mp')
 
-let (in_import,_) =
+let in_import =
   declare_object {(default_object "IMPORT MODULE") with
 		    cache_function = cache_import;
 		    open_function = (fun i o -> if i=1 then cache_import o);
@@ -840,7 +840,7 @@ let classify_include ((me,is_mod),substobjs) =
   Substitute ((me,is_mod),substobjs)
 
 let (in_include,out_include) =
-  declare_object {(default_object "INCLUDE") with
+  declare_object_full {(default_object "INCLUDE") with
     cache_function = cache_include;
     load_function = load_include;
     open_function = open_include;
diff --git a/library/goptions.ml b/library/goptions.ml
index 85d9fd77b..e047ab9a0 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -94,7 +94,7 @@ module MakeTable =
 	    if p' == p then obj else
 	      (f,p')
 	in
-        let (inGo,outGo) =
+        let inGo =
           Libobject.declare_object {(Libobject.default_object nick) with
                 Libobject.load_function = load_options;
 		Libobject.open_function = load_options;
@@ -235,18 +235,18 @@ let declare_option cast uncast
       That way I shouldn't collide with [nickname key] for any [key]. As [key]-s are
        lists of strings *without* spaces. *)
   let (write,lwrite,gwrite) = if sync then
-    let (ldecl_obj,_) = (* "Local": doesn't survive section or modules. *)
+    let ldecl_obj = (* "Local": doesn't survive section or modules. *)
       declare_object {(default_object ("L  "^nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun _ -> Dispose)}
     in
-    let (decl_obj,_) = (* default locality: survives sections but not modules. *)
+    let decl_obj = (* default locality: survives sections but not modules. *)
       declare_object {(default_object (nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun _ -> Dispose);
 		       discharge_function = (fun (_,v) -> Some v)}
     in
-    let (gdecl_obj,_) = (* "Global": survives section and modules. *)
+    let gdecl_obj = (* "Global": survives section and modules. *)
       declare_object {(default_object ("G  "^nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun v -> Substitute v);
diff --git a/library/heads.ml b/library/heads.ml
index 313050bbc..363443bbb 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -165,7 +165,7 @@ let discharge_head (_,(ref,k)) =
 let rebuild_head (ref,k) =
   (ref, compute_head ref)
 
-let (inHead, _) =
+let inHead =
   declare_object {(default_object "HEAD") with
     cache_function = cache_head;
     load_function = load_head;
diff --git a/library/impargs.ml b/library/impargs.ml
index daf264f6a..84097c840 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -300,8 +300,6 @@ let compute_manual_implicits env flags t enriching l =
   in
   merge 1 l autoimps
 
-let const v _ = v
-
 let compute_implicits_auto env f manual t =
   match manual with
   | [] ->
@@ -523,7 +521,7 @@ let rebuild_implicits (req,l) =
 let classify_implicits (req,_ as obj) =
   if req = ImplLocal then Dispose else Substitute obj
 
-let (inImplicits, _) =
+let inImplicits =
   declare_object {(default_object "IMPLICITS") with
     cache_function = cache_implicits;
     load_function = load_implicits;
diff --git a/library/lib.ml b/library/lib.ml
index 8c9153cd7..f0eea4355 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -252,12 +252,6 @@ let add_frozen_state () =
 
 (* Modules. *)
 
-
-let is_opened id = function
-    oname,(OpenedSection _ | OpenedModule _ | OpenedModtype _) when
-      basename (fst oname) = id -> true
-  | _ -> false
-
 let is_opening_node = function
     _,(OpenedSection _ | OpenedModule _ | OpenedModtype _) -> true
   | _ -> false
@@ -356,13 +350,6 @@ let contents_after = function
 
 (* Modules. *)
 
-let check_for_comp_unit () =
-  let is_decl = function (_,FrozenState _) -> false | _ -> true in
-  try
-    let _ = find_entry_p is_decl in
-    error "a module cannot be started after some declarations"
-  with Not_found -> ()
-
 (* TODO: use check_for_module ? *)
 let start_compilation s mp =
   if !comp_name <> None then
@@ -499,8 +486,6 @@ let add_section_constant kn =
 
 let replacement_context () = pi2 (List.hd !sectab)
 
-let variables_context () = pi1 (List.hd !sectab)
-
 let section_segment_of_constant con =
   Names.Cmap.find con (fst (pi3 (List.hd !sectab)))
 
@@ -595,7 +580,7 @@ let close_section () =
 (* Backtracking. *)
 
 let (inLabel,outLabel) =
-  declare_object {(default_object "DOT") with
+  declare_object_full {(default_object "DOT") with
 				classify_function = (fun _ -> Dispose)}
 
 let recache_decl = function
diff --git a/library/libnames.ml b/library/libnames.ml
index bb45369f2..e47ce86ca 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -195,8 +195,6 @@ module SpOrdered =
     let compare = sp_ord
   end
 
-module Spset = Set.Make(SpOrdered)
-module Sppred = Predicate.Make(SpOrdered)
 module Spmap = Map.Make(SpOrdered)
 
 let dirpath sp = let (p,_) = repr_path sp in p
diff --git a/library/libnames.mli b/library/libnames.mli
index f881f4b38..1f49b6a4f 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -107,7 +107,6 @@ val path_of_string : string -> full_path
 val string_of_path : full_path -> string
 val pr_path : full_path -> std_ppcmds
 
-module Sppred : Predicate.S with type elt = full_path
 module Spmap  : Map.S with type key = full_path
 
 val restrict_path : int -> full_path -> full_path
diff --git a/library/libobject.ml b/library/libobject.ml
index b44418b13..d9ffe1cd5 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -79,7 +79,7 @@ let object_tag lobj = Dyn.tag lobj
 let cache_tab =
   (Hashtbl.create 17 : (string,dynamic_object_declaration) Hashtbl.t)
 
-let declare_object odecl =
+let declare_object_full odecl =
   let na = odecl.object_name in
   let (infun,outfun) = Dyn.create na in
   let cacher (oname,lobj) =
@@ -122,6 +122,8 @@ let declare_object odecl =
 			     dyn_rebuild_function = rebuild };
   (infun,outfun)
 
+let declare_object odecl = fst (declare_object_full odecl)
+
 let missing_tab = (Hashtbl.create 17 : (string, unit) Hashtbl.t)
 
 (* this function describes how the cache, load, open, and export functions
diff --git a/library/libobject.mli b/library/libobject.mli
index 32cf9354f..ad4468fb8 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -85,15 +85,18 @@ val default_object : string -> 'a object_declaration
 val ident_subst_function : substitution * 'a -> 'a
 
 (** {6 ... } *)
-(** Given an object declaration, the function [declare_object]
+(** Given an object declaration, the function [declare_object_full]
    will hand back two functions, the "injection" and "projection"
    functions for dynamically typed library-objects. *)
 
 type obj
 
-val declare_object :
+val declare_object_full :
   'a object_declaration -> ('a -> obj) * (obj -> 'a)
 
+val declare_object :
+  'a object_declaration -> ('a -> obj)
+
 val object_tag : obj -> string
 
 val cache_object : object_name * obj -> unit
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;
diff --git a/library/nameops.ml b/library/nameops.ml
index e8c5b3d05..799b8ebe1 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -110,8 +110,6 @@ let add_prefix s id = id_of_string (s ^ string_of_id id)
 
 let atompart_of_id id = fst (repr_ident id)
 
-let lift_ident = lift_subscript
-
 (* Names *)
 
 let out_name = function
diff --git a/library/nametab.ml b/library/nametab.ml
index 7ee4b3920..e43ae650c 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -378,7 +378,6 @@ let locate_modtype qid = SpTab.locate qid !the_modtypetab
 let full_name_modtype qid = SpTab.user_name qid !the_modtypetab
 
 let locate_tactic qid = SpTab.locate qid !the_tactictab
-let full_name_tactic qid = SpTab.user_name qid !the_tactictab
 
 let locate_dir qid = DirTab.locate qid !the_dirtab
 
@@ -411,11 +410,6 @@ let locate_constant qid =
     | TrueGlobal (ConstRef kn) -> kn
     | _ -> raise Not_found
 
-let locate_mind qid =
-  match locate_extended qid with
-    | TrueGlobal (IndRef (kn,0)) -> kn
-    | _ -> raise Not_found
-
 let global_of_path sp =
   match SpTab.find sp !the_ccitab with
     | TrueGlobal ref -> ref
@@ -423,9 +417,6 @@ let global_of_path sp =
 
 let extended_global_of_path sp = SpTab.find sp !the_ccitab
 
-let locate_in_absolute_module dir id =
-  global_of_path (make_path dir id)
-
 let global r =
   let (loc,qid) = qualid_of_reference r in
   try match locate_extended qid with
@@ -449,8 +440,6 @@ let exists_module = exists_dir
 
 let exists_modtype sp = SpTab.exists sp !the_modtypetab
 
-let exists_tactic sp = SpTab.exists sp !the_tactictab
-
 (* Reverse locate functions ***********************************************)
 
 let path_of_global ref =