summaryrefslogtreecommitdiff
path: root/src/util.mli
diff options
context:
space:
mode:
Diffstat (limited to 'src/util.mli')
-rw-r--r--src/util.mli5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/util.mli b/src/util.mli
index f1182c61..11588de2 100644
--- a/src/util.mli
+++ b/src/util.mli
@@ -40,6 +40,11 @@
(* SUCH DAMAGE. *)
(**************************************************************************)
+(* Last element of a list *)
+val last : 'a list -> 'a
+
+val butlast : 'a list -> 'a list
+
(** Mixed useful things *)
module Duplicate(S : Set.S) : sig
type dups =