From 691d37218de76b0bf8084653ee85ddae43ff74a8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 7 Sep 1999 12:51:05 +0000
Subject: mise en place commandes minicoq

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@42 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 6 ++++++
 lib/util.mli | 4 ++++
 2 files changed, 10 insertions(+)

(limited to 'lib')

diff --git a/lib/util.ml b/lib/util.ml
index fb50d1e4e5..deb810cdd1 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -259,6 +259,12 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset = Set.Make(struct type t = int let compare = compare end)
 
+let option_app f = function
+  | None -> None
+  | Some x -> Some (f x)
+
+(* Time stamps. *)
+
 type time_stamp = float
 
 let get_time_stamp () = Unix.time()
diff --git a/lib/util.mli b/lib/util.mli
index 98296264f9..0ef34a8418 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -72,6 +72,10 @@ type ('a,'b) union = Inl of 'a | Inr of 'b
 
 module Intset : Set.S with type elt = int
 
+val option_app : ('a -> 'b) -> 'a option -> 'b option
+
+(*s Time stamps. *)
+
 type time_stamp
 
 val get_time_stamp : unit -> time_stamp
-- 
cgit v1.2.3