2 files changed, 10 insertions, 1 deletions
diff --git a/utils/misc.ml b/utils/misc.ml
index 529484692..390abd799 100644
--- a/utils/misc.ml
+++ b/utils/misc.ml
@@ -54,6 +54,13 @@ let rec list_remove x = function
   | hd :: tl ->
       if hd = x then tl else hd :: list_remove x tl
 
+let rec split_last = function
+    [] -> assert false
+  | [x] -> ([], x)
+  | hd :: tl ->
+      let (lst, last) = split_last tl in
+      (hd :: lst, last)
+
 (* Options *)
 
 let may f = function
diff --git a/utils/misc.mli b/utils/misc.mli
index 969e97818..f3777c518 100644
--- a/utils/misc.mli
+++ b/utils/misc.mli
@@ -28,7 +28,9 @@ val replicate_list: 'a -> int -> 'a list
            all identical to [elem]. *)
 val list_remove: 'a -> 'a list -> 'a list
         (* [list_remove x l] returns a copy of [l] with the first
-           element equal to [x] removed *)
+           element equal to [x] removed. *)
+val split_last: 'a list -> 'a list * 'a
+        (* Return the last element and the other elements of the given list. *)
 
 val may: ('a -> unit) -> 'a option -> unit
 val may_map: ('a -> 'b) -> 'a option -> 'b option