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

8 files changed, 0 insertions, 373 deletions

diff --git a/lib/gset.ml b/lib/gset.ml
deleted file mode 100644
index 9842595006..0000000000
--- a/lib/gset.ml
+++ /dev/null
@@ -1,240 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* Sets using the generic comparison function of ocaml. Code borrowed from
-   the ocaml standard library. *)
-
-    type 'a t = Empty | Node of 'a t * 'a * 'a t * int
-
-    (* Sets are represented by balanced binary trees (the heights of the
-       children differ by at most 2 *)
-
-    let height = function
-        Empty -> 0
-      | Node(_, _, _, h) -> h
-
-    (* Creates a new node with left son l, value x and right son r.
-       l and r must be balanced and | height l - height r | <= 2.
-       Inline expansion of height for better speed. *)
-
-    let create l x r =
-      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
-      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
-      Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
-
-    (* Same as create, but performs one step of rebalancing if necessary.
-       Assumes l and r balanced.
-       Inline expansion of create for better speed in the most frequent case
-       where no rebalancing is required. *)
-
-    let bal l x r =
-      let hl = match l with Empty -> 0 | Node(_,_,_,h) -> h in
-      let hr = match r with Empty -> 0 | Node(_,_,_,h) -> h in
-      if hl > hr + 2 then begin
-        match l with
-          Empty -> invalid_arg "Set.bal"
-        | Node(ll, lv, lr, _) ->
-            if height ll >= height lr then
-              create ll lv (create lr x r)
-            else begin
-              match lr with
-                Empty -> invalid_arg "Set.bal"
-              | Node(lrl, lrv, lrr, _)->
-                  create (create ll lv lrl) lrv (create lrr x r)
-            end
-      end else if hr > hl + 2 then begin
-        match r with
-          Empty -> invalid_arg "Set.bal"
-        | Node(rl, rv, rr, _) ->
-            if height rr >= height rl then
-              create (create l x rl) rv rr
-            else begin
-              match rl with
-                Empty -> invalid_arg "Set.bal"
-              | Node(rll, rlv, rlr, _) ->
-                  create (create l x rll) rlv (create rlr rv rr)
-            end
-      end else
-        Node(l, x, r, (if hl >= hr then hl + 1 else hr + 1))
-
-    (* Same as bal, but repeat rebalancing until the final result
-       is balanced. *)
-
-    let rec join l x r =
-      match bal l x r with
-        Empty -> invalid_arg "Set.join"
-      | Node(l', x', r', _) as t' ->
-          let d = height l' - height r' in
-          if d < -2 or d > 2 then join l' x' r' else t'
-
-    (* Merge two trees l and r into one.
-       All elements of l must precede the elements of r.
-       Assumes | height l - height r | <= 2. *)
-
-    let rec merge t1 t2 =
-      match (t1, t2) with
-        (Empty, t) -> t
-      | (t, Empty) -> t
-      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
-          bal l1 v1 (bal (merge r1 l2) v2 r2)
-
-    (* Same as merge, but does not assume anything about l and r. *)
-
-    let rec concat t1 t2 =
-      match (t1, t2) with
-        (Empty, t) -> t
-      | (t, Empty) -> t
-      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
-          join l1 v1 (join (concat r1 l2) v2 r2)
-
-    (* Splitting *)
-
-    let rec split x = function
-        Empty ->
-          (Empty, None, Empty)
-      | Node(l, v, r, _) ->
-          let c = Pervasives.compare x v in
-          if c = 0 then (l, Some v, r)
-          else if c < 0 then
-            let (ll, vl, rl) = split x l in (ll, vl, join rl v r)
-          else
-            let (lr, vr, rr) = split x r in (join l v lr, vr, rr)
-
-    (* Implementation of the set operations *)
-
-    let empty = Empty
-
-    let is_empty = function Empty -> true | _ -> false
-
-    let rec mem x = function
-        Empty -> false
-      | Node(l, v, r, _) ->
-          let c = Pervasives.compare x v in
-          c = 0 || mem x (if c < 0 then l else r)
-
-    let rec add x = function
-        Empty -> Node(Empty, x, Empty, 1)
-      | Node(l, v, r, _) as t ->
-          let c = Pervasives.compare x v in
-          if c = 0 then t else
-          if c < 0 then bal (add x l) v r else bal l v (add x r)
-
-    let singleton x = Node(Empty, x, Empty, 1)
-
-    let rec remove x = function
-        Empty -> Empty
-      | Node(l, v, r, _) ->
-          let c = Pervasives.compare x v in
-          if c = 0 then merge l r else
-          if c < 0 then bal (remove x l) v r else bal l v (remove x r)
-
-    let rec union s1 s2 =
-      match (s1, s2) with
-        (Empty, t2) -> t2
-      | (t1, Empty) -> t1
-      | (Node(l1, v1, r1, h1), Node(l2, v2, r2, h2)) ->
-          if h1 >= h2 then
-            if h2 = 1 then add v2 s1 else begin
-              let (l2, _, r2) = split v1 s2 in
-              join (union l1 l2) v1 (union r1 r2)
-            end
-          else
-            if h1 = 1 then add v1 s2 else begin
-              let (l1, _, r1) = split v2 s1 in
-              join (union l1 l2) v2 (union r1 r2)
-            end
-
-    let rec inter s1 s2 =
-      match (s1, s2) with
-        (Empty, t2) -> Empty
-      | (t1, Empty) -> Empty
-      | (Node(l1, v1, r1, _), t2) ->
-          match split v1 t2 with
-            (l2, None, r2) ->
-              concat (inter l1 l2) (inter r1 r2)
-          | (l2, Some _, r2) ->
-              join (inter l1 l2) v1 (inter r1 r2)
-
-    let rec diff s1 s2 =
-      match (s1, s2) with
-        (Empty, t2) -> Empty
-      | (t1, Empty) -> t1
-      | (Node(l1, v1, r1, _), t2) ->
-          match split v1 t2 with
-            (l2, None, r2) ->
-              join (diff l1 l2) v1 (diff r1 r2)
-          | (l2, Some _, r2) ->
-              concat (diff l1 l2) (diff r1 r2)
-
-    let rec compare_aux l1 l2 =
-        match (l1, l2) with
-        ([], []) -> 0
-      | ([], _)  -> -1
-      | (_, []) -> 1
-      | (Empty :: t1, Empty :: t2) ->
-          compare_aux t1 t2
-      | (Node(Empty, v1, r1, _) :: t1, Node(Empty, v2, r2, _) :: t2) ->
-          let c = compare v1 v2 in
-          if c <> 0 then c else compare_aux (r1::t1) (r2::t2)
-      | (Node(l1, v1, r1, _) :: t1, t2) ->
-          compare_aux (l1 :: Node(Empty, v1, r1, 0) :: t1) t2
-      | (t1, Node(l2, v2, r2, _) :: t2) ->
-          compare_aux t1 (l2 :: Node(Empty, v2, r2, 0) :: t2)
-
-    let compare s1 s2 =
-      compare_aux [s1] [s2]
-
-    let equal s1 s2 =
-      compare s1 s2 = 0
-
-    let rec subset s1 s2 =
-      match (s1, s2) with
-        Empty, _ ->
-          true
-      | _, Empty ->
-          false
-      | Node (l1, v1, r1, _), (Node (l2, v2, r2, _) as t2) ->
-          let c = Pervasives.compare v1 v2 in
-          if c = 0 then
-            subset l1 l2 && subset r1 r2
-          else if c < 0 then
-            subset (Node (l1, v1, Empty, 0)) l2 && subset r1 t2
-          else
-            subset (Node (Empty, v1, r1, 0)) r2 && subset l1 t2
-
-    let rec iter f = function
-        Empty -> ()
-      | Node(l, v, r, _) -> iter f l; f v; iter f r
-
-    let rec fold f s accu =
-      match s with
-        Empty -> accu
-      | Node(l, v, r, _) -> fold f l (f v (fold f r accu))
-
-    let rec cardinal = function
-        Empty -> 0
-      | Node(l, v, r, _) -> cardinal l + 1 + cardinal r
-
-    let rec elements_aux accu = function
-        Empty -> accu
-      | Node(l, v, r, _) -> elements_aux (v :: elements_aux accu r) l
-
-    let elements s =
-      elements_aux [] s
-
-    let rec min_elt = function
-        Empty -> raise Not_found
-      | Node(Empty, v, r, _) -> v
-      | Node(l, v, r, _) -> min_elt l
-
-    let rec max_elt = function
-        Empty -> raise Not_found
-      | Node(l, v, Empty, _) -> v
-      | Node(l, v, r, _) -> max_elt r
-
-    let choose = min_elt
diff --git a/lib/gset.mli b/lib/gset.mli
deleted file mode 100644
index ae5e13e9e3..0000000000
--- a/lib/gset.mli
+++ /dev/null
@@ -1,32 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Sets using the generic comparison function of ocaml. Same interface as
-   the module [Set] from the ocaml standard library. *)
-
-type 'a t
-
-val empty : 'a t
-val is_empty : 'a t -> bool
-val mem : 'a -> 'a t -> bool
-val add : 'a -> 'a t -> 'a t
-val singleton : 'a -> 'a t
-val remove : 'a -> 'a t -> 'a t
-val union : 'a t -> 'a t -> 'a t
-val inter : 'a t -> 'a t -> 'a t
-val diff : 'a t -> 'a t -> 'a t
-val compare : 'a t -> 'a t -> int
-val equal : 'a t -> 'a t -> bool
-val subset : 'a t -> 'a t -> bool
-val iter : ('a -> unit) -> 'a t -> unit
-val fold : ('a -> 'b -> 'b) -> 'a t -> 'b -> 'b
-val cardinal : 'a t -> int
-val elements : 'a t -> 'a list
-val min_elt : 'a t -> 'a
-val max_elt : 'a t -> 'a
-val choose : 'a t -> 'a
diff --git a/lib/lib.mllib b/lib/lib.mllib
index c3982a8c96..0607ae50e6 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -10,11 +10,9 @@ Hashcons
 Dyn
 System
 Envars
-Gset
 Gmap
 Fset
 Fmap
-Tlm
 Tries
 Gmapl
 Profile
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 37d63b3601..854e4b49ca 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -273,11 +273,6 @@ let pp_dirs ft =
 
 (* pretty print on stdout and stderr *)
 
-let pp_std_dirs = pp_dirs !std_ft
-let pp_err_dirs = pp_dirs !err_ft
-
-let ppcmds x = Ppdir_ppcmds x
-
 (* Special chars for emacs, to detect warnings inside goal output *)
 let emacs_warning_start_string = String.make 1 (Char.chr 254)
 let emacs_warning_end_string = String.make 1 (Char.chr 255)
diff --git a/lib/profile.ml b/lib/profile.ml
index fe86fac590..53ba0c19b3 100644
--- a/lib/profile.ml
+++ b/lib/profile.ml
@@ -9,7 +9,6 @@
 open Gc
 
 let word_length = Sys.word_size / 8
-let int_size = Sys.word_size - 1
 
 let float_of_time t = float_of_int t /. 100.
 let time_of_float f = int_of_float (f *. 100.)
@@ -352,7 +351,6 @@ let close_profile print =
 	end
     | _ -> failwith "Inconsistency"
 
-let append_profile () = close_profile false
 let print_profile () = close_profile true
 
 let declare_profile name =
diff --git a/lib/segmenttree.ml b/lib/segmenttree.ml
index 2a7f9df0ed..9ce348a0bd 100644
--- a/lib/segmenttree.ml
+++ b/lib/segmenttree.ml
@@ -40,7 +40,6 @@ type domain =
 type 'a t = (domain * 'a option) array
 
 (** The root is the first item of the array. *)
-let is_root i = (i = 0)
 
 (** Standard layout for left child. *)
 let left_child i = 2 * i + 1
diff --git a/lib/tlm.ml b/lib/tlm.ml
deleted file mode 100644
index 4c2287dd2a..0000000000
--- a/lib/tlm.ml
+++ /dev/null
@@ -1,61 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-type ('a,'b) t = Node of 'b Gset.t * ('a, ('a,'b) t) Gmap.t
-
-let empty = Node (Gset.empty, Gmap.empty)
-
-let map (Node (_,m)) lbl = Gmap.find lbl m
-
-let xtract (Node (hereset,_)) = Gset.elements hereset
-
-let dom (Node (_,m)) = Gmap.dom m
-
-let in_dom (Node (_,m)) lbl = Gmap.mem lbl m
-
-let is_empty_node (Node(a,b)) = (Gset.elements a = []) & (Gmap.to_list b = [])
-
-let assure_arc m lbl =
-  if Gmap.mem lbl m then
-    m
-  else
-    Gmap.add lbl (Node (Gset.empty,Gmap.empty)) m
-
-let cleanse_arcs (Node (hereset,m)) =
-  let l = Gmap.rng m in
-  Node(hereset, if List.for_all is_empty_node l then Gmap.empty else m)
-
-let rec at_path f (Node (hereset,m)) = function
-  | [] ->
-      cleanse_arcs (Node(f hereset,m))
-  | h::t ->
-      let m = assure_arc m h in
-      cleanse_arcs (Node(hereset,
-                         Gmap.add h (at_path f (Gmap.find h m) t) m))
-
-let add tm (path,v) =
-  at_path (fun hereset -> Gset.add v hereset) tm path
-
-let rmv tm (path,v) =
-  at_path (fun hereset -> Gset.remove v hereset) tm path
-
-let app f tlm =
-  let rec apprec pfx (Node(hereset,m)) =
-    let path = List.rev pfx in
-    Gset.iter (fun v -> f(path,v)) hereset;
-    Gmap.iter (fun l tm -> apprec (l::pfx) tm) m
-  in
-  apprec [] tlm
-
-let to_list tlm =
-  let rec torec pfx (Node(hereset,m)) =
-    let path = List.rev pfx in
-    List.flatten((List.map (fun v -> (path,v)) (Gset.elements hereset))::
-		 (List.map (fun (l,tm) -> torec (l::pfx) tm) (Gmap.to_list m)))
-  in
-  torec [] tlm
diff --git a/lib/tlm.mli b/lib/tlm.mli
deleted file mode 100644
index 73668ff446..0000000000
--- a/lib/tlm.mli
+++ /dev/null
@@ -1,30 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Tries. This module implements a data structure [('a,'b) t] mapping lists
-   of values of type ['a] to sets (as lists) of values of type ['b]. *)
-
-type ('a,'b) t
-
-val empty : ('a,'b) t
-
-(** Work on labels, not on paths. *)
-
-val map : ('a,'b) t -> 'a -> ('a,'b) t
-val xtract : ('a,'b) t -> 'b list
-val dom : ('a,'b) t -> 'a list
-val in_dom : ('a,'b) t -> 'a -> bool
-
-(** Work on paths, not on labels. *)
-
-val add : ('a,'b) t -> 'a list * 'b -> ('a,'b) t
-val rmv : ('a,'b) t -> ('a list * 'b) -> ('a,'b) t
-
-val app : (('a list * 'b) -> unit) -> ('a,'b) t -> unit
-val to_list : ('a,'b) t -> ('a list * 'b) list
-