From a417d138c0a8abc028486c20d59e4f2e82f456ef Mon Sep 17 00:00:00 2001
From: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
Date: Fri, 12 Dec 2014 15:19:10 +0100
Subject: Searchxxx now search also the hypothesis and support goal selector.

Documentation also updated.
---
 lib/util.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'lib/util.mli')

diff --git a/lib/util.mli b/lib/util.mli
index 86720fe47..bcb1b6265 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -89,6 +89,10 @@ val iterate : ('a -> 'a) -> int -> 'a -> 'a
 val repeat : int -> ('a -> unit) -> 'a -> unit
 val app_opt : ('a -> 'a) option -> 'a -> 'a
 
+(** [un_opt opt default] returns the content of [opt] if possible and
+    default otherwise. *)
+val un_opt : 'a option -> 'a -> 'a
+
 (** {6 Delayed computations. } *)
 
 type 'a delayed = unit -> 'a
-- 
cgit v1.2.3