From 987648c2db72d8cc135b144a584072a5c8ef5bfb Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Tue, 16 Dec 2014 15:57:33 +0100
Subject: [PATCH] Added a somewhat unusual [Option.project].

---
 src/option.ml  | 6 ++++++
 src/option.mli | 1 +
 2 files changed, 7 insertions(+)

diff --git a/src/option.ml b/src/option.ml
index 5898eac7..ab66e8d4 100644
--- a/src/option.ml
+++ b/src/option.ml
@@ -18,3 +18,9 @@ let fold f o accu =
   | Some x ->
       f x accu
 
+let project = function
+  | Some x ->
+      x
+  | None ->
+      (* Presumably, an error message has already been printed. *)
+      exit 1
diff --git a/src/option.mli b/src/option.mli
index 832f63d7..162e8325 100644
--- a/src/option.mli
+++ b/src/option.mli
@@ -1,3 +1,4 @@
 val map: ('a -> 'b) -> 'a option -> 'b option
 val iter: ('a -> unit) -> 'a option -> unit
 val fold: ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b
+val project: 'a option -> 'a (* careful: calls [exit 1] in case of failure *)
-- 
GitLab