diff --git a/src/option.ml b/src/option.ml index 5898eac7f64cfb9a9910ee3237719843666eea0a..ab66e8d471037e5b86e6243504436293dc951f58 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 832f63d717976e9539df3b3934e144d6119e9ab8..162e8325230182e8600d2b89ff1e2934e7d104d1 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 *)