diff options
author | Sébastien Dailly <sebastien@chimrod.com> | 2018-01-19 11:24:29 +0100 |
---|---|---|
committer | Sébastien Dailly <sebastien@chimrod.com> | 2018-01-25 17:17:15 +0100 |
commit | 112ab4b1c396fc2117191297227d8e411f9b9bb3 (patch) | |
tree | f6d06ef60c696b43d48e2cd8e2f7f426a03b3706 /src/splay.mli | |
parent | 098ac444e731d7674d8910264ae58fb876618a5a (diff) |
Better memory management
Diffstat (limited to 'src/splay.mli')
-rwxr-xr-x | src/splay.mli | 30 |
1 files changed, 0 insertions, 30 deletions
diff --git a/src/splay.mli b/src/splay.mli deleted file mode 100755 index 41c1a5a..0000000 --- a/src/splay.mli +++ /dev/null @@ -1,30 +0,0 @@ -module type KEY = sig
-
- type 'a t
-
- val comp: 'a t -> 'b t -> ('a, 'b) Tools.cmp
-
- val repr: Format.formatter -> 'a t -> unit
-
-end
-
-module Make (El : KEY) : sig
-
- type t
-
- (** Create an empty tree *)
- val empty: t
-
- (** Return the element in the tree with the given key *)
- val find: 'a El.t -> t -> 'a
-
- (** Add one element in the tree *)
- val add: 'a El.t -> 'a -> t -> t
-
- (** Check if the key exists *)
- val member: 'a El.t -> t -> bool
-
- (** Represent the content in dot syntax *)
- val repr: Format.formatter -> t -> unit
-
-end
|