aboutsummaryrefslogtreecommitdiff
path: root/lib/tlm.mli
diff options
context:
space:
mode:
authorletouzey2010-09-24 13:14:17 +0000
committerletouzey2010-09-24 13:14:17 +0000
commitc789e243ff599db876e94a5ab2a13ff98baa0d6c (patch)
tree6dffe51299d60f2fb9ad8fa0a90c5b8a2cd119d9 /lib/tlm.mli
parent61222d6bfb2fddd8608bea4056af2e9541819510 (diff)
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
Diffstat (limited to 'lib/tlm.mli')
-rw-r--r--lib/tlm.mli30
1 files changed, 0 insertions, 30 deletions
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
-