diff --git a/heap.ml b/heap.ml
index 1c6dd28a..01830aec 100644
--- a/heap.ml
+++ b/heap.ml
@@ -23,7 +23,7 @@ OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
-(** {1 Binary heaps} *)
+(** {1 Imperative priority queue} *)
 
 type 'a t = {
   tree: 'a tree;
@@ -64,6 +64,9 @@ let min heap =
 (** Discard the minimal element *)
 let junk heap = failwith "TODO: Heap.junk"
 
+(** Remove and return the mininal value (or raise Invalid_argument) *)
+let pop heap =
+
 (** Iterate on the elements, in an unspecified order *)
 let iter heap k =
   let rec iter tree = match tree with
diff --git a/heap.mli b/heap.mli
index 36a10730..c34c4a4a 100644
--- a/heap.mli
+++ b/heap.mli
@@ -23,15 +23,15 @@ OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)
 
-(** {1 Binary heaps} *)
+(** {1 Imperative priority queue} *)
 
 type 'a t
   (** A heap containing values of type 'a *)
 
-val empty : lt:('a -> 'a -> bool) -> 'a t
+val empty : cmp:('a -> 'a -> int) -> 'a t
   (** Create an empty heap *)
 
-val insert : 'a t -> 'a -> 'a t
+val insert : 'a t -> 'a -> unit
   (** Insert a value in the heap *)
 
 val is_empty : 'a t -> bool
@@ -40,8 +40,11 @@ val is_empty : 'a t -> bool
 val min : 'a t -> 'a
   (** Access the minimal value of the heap, or raises Invalid_argument *)
 
-val junk : 'a t -> 'a t
+val junk : 'a t -> unit
   (** Discard the minimal element *)
 
+val pop : 'a t -> 'a
+  (** Remove and return the mininal value (or raise Invalid_argument) *)
+
 val iter : 'a t -> ('a -> unit) -> unit
   (** Iterate on the elements, in an unspecified order *)
diff --git a/splayTree.ml b/splayTree.ml
new file mode 100644
index 00000000..6777ed85
--- /dev/null
+++ b/splayTree.ml
@@ -0,0 +1,65 @@
+(*
+Copyright (c) 2013, Simon Cruanes
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.  Redistributions in binary
+form must reproduce the above copyright notice, this list of conditions and the
+following disclaimer in the documentation and/or other materials provided with
+the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*)
+
+(** {1 Splay trees} *)
+
+(** See http://en.wikipedia.org/wiki/Splay_tree and
+    Okasaki's "purely functional data structures" p46 *)
+
+type ('a, 'b) t = (('a, 'b) tree * ('a -> 'a -> int))
+  (** A splay tree with the given comparison function *)
+and ('a, 'b) tree =
+  | Empty
+  | Node of (('a,'b) tree * 'a * 'b * ('a,'b) tree)
+  (** A splay tree containing values of type 'a *)
+
+let empty ~cmp =
+  (Empty, cmp)
+
+let is_empty (tree, _) =
+  match tree with
+  | Empty -> true
+  | Node _ -> false
+
+let rec bigger ~cmp pivot tree =
+  match tree with
+  | Empty -> Empty
+  | Node (a, x, x_val, b) ->
+    if cmp x pivot <= 0
+      then bigger ~cmp pivot b
+      else match a with
+        | Empty -> Node (Empty, x, x_val, b)
+        | Node (a1, y, y_val, a2) ->
+          if cmp y pivot <= 0
+            then Node (bigger ~cmp pivot a2, x, x_val, b)
+            else Node (bigger ~cmp pivot a1, y, y_val, Node (a2, x, x_val, b))
+
+let rec smaller ~cmp pivot tree =
+
+(** Insert the pair (key -> value) in the tree *)
+let insert (tree, cmp) k v =
+  let tree' = Node (smaller ~cmp k tree, k, v, bigger ~cmp k tree) in
+  tree', cmp
+
diff --git a/splayTree.mli b/splayTree.mli
new file mode 100644
index 00000000..08adcc44
--- /dev/null
+++ b/splayTree.mli
@@ -0,0 +1,65 @@
+(*
+Copyright (c) 2013, Simon Cruanes
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+Redistributions of source code must retain the above copyright notice, this
+list of conditions and the following disclaimer.  Redistributions in binary
+form must reproduce the above copyright notice, this list of conditions and the
+following disclaimer in the documentation and/or other materials provided with
+the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+*)
+
+(** {1 Splay trees} *)
+
+(** See http://en.wikipedia.org/wiki/Splay_tree and
+    Okasaki's "purely functional data structures" p46 *)
+
+type ('a, 'b) t
+  (** A functional splay tree *)
+
+val empty : cmp:('a -> 'a -> bool) -> ('a, 'b) t
+  (** Empty splay tree using the given comparison function *)
+
+val is_empty : (_, _) t -> bool
+  (** Check whether the tree is empty *)
+
+val insert : ('a, 'b) t -> 'a -> 'b -> ('a, 'b) t
+  (** Insert the pair (key -> value) in the tree *)
+
+val replace : ('a, 'b) t -> 'a -> 'b -> ('a, 'b) t
+  (** Insert the pair (key -> value) into the tree, replacing
+      the previous binding (if any). It replaces at most one
+      binding. *)
+
+val remove : ('a, 'b) t -> 'a -> ('a, 'b) t
+  (** Remove an element by its key, returns the splayed tree *)
+
+val top : ('a, b') t -> 'a * 'b
+  (** Returns the top value, or raise Not_found is empty *)
+
+val min : ('a, 'b) t -> 'a * 'b * ('a, b') t
+  (** Access minimum value *)
+
+val find : ('a, 'b) t -> 'a -> 'b * ('a, 'b) t
+  (** Find the value for the given key (or raise Not_found).
+      It also returns the splayed tree *)
+
+val size : (_, _) t -> int
+  (** Number of elements (linear) *)
+
+val iter : ('a -> 'b -> unit) -> ('a, 'b) t -> unit
+  (** Iterate on elements *)