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

7 files changed, 20 insertions, 20 deletions

diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index 34b32c0a7a..b800170de3 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -37,7 +37,7 @@ let set_trace b = trace := b
 let timeout = ref 10
 let set_timeout n = timeout := n
 
-let (dp_timeout_obj,_) =
+let dp_timeout_obj =
   declare_object
     {(default_object "Dp_timeout") with
        cache_function = (fun (_,x) -> set_timeout x);
@@ -45,7 +45,7 @@ let (dp_timeout_obj,_) =
 
 let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
 
-let (dp_debug_obj,_) =
+let dp_debug_obj =
   declare_object
     {(default_object "Dp_debug") with
        cache_function = (fun (_,x) -> set_debug x);
@@ -53,7 +53,7 @@ let (dp_debug_obj,_) =
 
 let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
 
-let (dp_trace_obj,_) =
+let dp_trace_obj =
   declare_object
     {(default_object "Dp_trace") with
        cache_function = (fun (_,x) -> set_trace x);
@@ -826,7 +826,7 @@ let prelude_files = ref ([] : string list)
 
 let set_prelude l = prelude_files := l
 
-let (dp_prelude_obj,_) =
+let dp_prelude_obj =
   declare_object
     {(default_object "Dp_prelude") with
        cache_function = (fun (_,x) -> set_prelude x);
@@ -1088,7 +1088,7 @@ let dp_hint l =
   in
   List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
 
-let (dp_hint_obj,_) =
+let dp_hint_obj =
   declare_object
     {(default_object "Dp_hint") with
        cache_function = (fun (_,l) -> dp_hint l);
@@ -1114,7 +1114,7 @@ let dp_predefined qid s =
   with NotFO ->
     msg_warning (str " ignored (not a first order declaration)")
 
-let (dp_predefined_obj,_) =
+let dp_predefined_obj =
   declare_object
     {(default_object "Dp_predefined") with
        cache_function = (fun (_,(id,s)) -> dp_predefined id s);
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 5457d2e8c2..a292dec2f9 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -459,7 +459,7 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let (extr_lang,_) =
+let extr_lang =
   declare_object
     {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
@@ -491,7 +491,7 @@ let add_inline_entries b l =
 
 (* Registration of operations for rollback. *)
 
-let (inline_extraction,_) =
+let inline_extraction =
   declare_object
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
@@ -534,7 +534,7 @@ let print_extraction_inline () =
 
 (* Reset part *)
 
-let (reset_inline,_) =
+let reset_inline =
   declare_object
     {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
@@ -573,7 +573,7 @@ let add_implicits r l =
 
 (* Registration of operations for rollback. *)
 
-let (implicit_extraction,_) =
+let implicit_extraction =
   declare_object
     {(default_object "Extraction Implicit") with
        cache_function = (fun (_,(r,l)) -> add_implicits r l);
@@ -633,7 +633,7 @@ let add_blacklist_entries l =
 
 (* Registration of operations for rollback. *)
 
-let (blacklist_extraction,_) =
+let blacklist_extraction =
   declare_object
     {(default_object "Extraction Blacklist") with
        cache_function = (fun (_,l) -> add_blacklist_entries l);
@@ -661,7 +661,7 @@ let print_extraction_blacklist () =
 
 (* Reset part *)
 
-let (reset_blacklist,_) =
+let reset_blacklist =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
        cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
@@ -707,7 +707,7 @@ let find_custom_match pv =
 
 (* Registration of operations for rollback. *)
 
-let (in_customs,_) =
+let in_customs =
   declare_object
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
@@ -722,7 +722,7 @@ let _ = declare_summary "ML extractions"
 	    unfreeze_function = ((:=) customs);
 	    init_function = (fun () -> customs := Refmap'.empty) }
 
-let (in_custom_matchs,_) =
+let in_custom_matchs =
   declare_object
     {(default_object "ML extractions custom matchs") with
        cache_function = (fun (_,(r,s)) -> add_custom_match r s);
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index d4ced4139a..1cba563eaf 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -65,7 +65,7 @@ let subst_addfield (subst,(typ,th as obj)) =
       (typ',th')
 
 (* Declaration of the Add Field library object *)
-let (in_addfield,out_addfield)=
+let in_addfield =
   Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with
        Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
        Libobject.cache_function = cache_addfield;
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ff7089613f..002fb70986 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -362,7 +362,7 @@ let pr_table tb =
   let l = Cmap.fold (fun k v acc -> v::acc) tb [] in
   Util.prlist_with_sep fnl pr_info l
 
-let in_Function,out_Function =
+let in_Function =
   Libobject.declare_object
     {(Libobject.default_object "FUNCTIONS_DB") with
        Libobject.cache_function = cache_Function;
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 8b977e5dce..7588e6a2fa 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -262,7 +262,7 @@ let subst_th (subst,(c,th as obj)) =
       (c',th')
 
 
-let (theory_to_obj, obj_to_theory) =
+let theory_to_obj =
   let cache_th (_,(c, th)) = theories_map_add (c,th) in
   declare_object {(default_object "tactic-ring-theory") with
 		    open_function = (fun i o -> if i=1 then cache_th o);
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index fa0e76841a..052406867d 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -440,7 +440,7 @@ let subst_th (subst,th) =
       ring_post_tac = posttac' }
 
 
-let (theory_to_obj, obj_to_theory) =
+let theory_to_obj =
   let cache_th (name,th) = add_entry name th in
   declare_object
     {(default_object "tactic-new-ring-theory") with
@@ -1016,7 +1016,7 @@ let subst_th (subst,th) =
       field_pre_tac = pretac';
       field_post_tac = posttac' }
 
-let (ftheory_to_obj, obj_to_ftheory) =
+let ftheory_to_obj =
   let cache_th (name,th) = add_field_entry name th in
   declare_object
     {(default_object "tactic-new-field-theory") with
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 591e01c04e..22cc745f6d 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -153,7 +153,7 @@ let _ =
 
 let progmap_union = ProgMap.fold ProgMap.add
 
-let (input,output) =
+let input =
   declare_object
     { (default_object "Program state") with
       classify_function = (fun () ->