From d47c178be6e5dc52fedbb312fc51673623608994 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 28 Oct 2014 15:29:52 +0100
Subject: Add an [Info Level] option to print info traces automatically.

[Set Info Level n] prints all info traces at level [n]. [Unset Info Level] stops the automatic printing of info traces. The unfolding level [n] can be overloaded by local [Info m tac] calls.
---
 lib/option.ml  | 8 ++++++++
 lib/option.mli | 6 ++++++
 2 files changed, 14 insertions(+)

(limited to 'lib')

diff --git a/lib/option.ml b/lib/option.ml
index abdae892f2..35f9bd7d1e 100644
--- a/lib/option.ml
+++ b/lib/option.ml
@@ -64,6 +64,14 @@ let flatten = function
   | _ -> None
 
 
+(** [append x y] is the first element of the concatenation of [x] and
+    [y] seen as lists. *)
+let append o1 o2 =
+  match o1 with
+  | Some _ -> o1
+  | None  -> o2
+
+
 (** {6 "Iterators"} ***)
 
 (** [iter f x] executes [f y] if [x] equals [Some y]. It does nothing
diff --git a/lib/option.mli b/lib/option.mli
index af8696a5e4..e9d76572e3 100644
--- a/lib/option.mli
+++ b/lib/option.mli
@@ -47,6 +47,12 @@ val init : bool -> 'a -> 'a option
 (** [flatten x] is [Some y] if [x] is [Some (Some y)] and [None] otherwise. *)
 val flatten : 'a option option -> 'a option
 
+(** [append x y] is the first element of the concatenation of [x] and
+    [y] seen as lists.  In other words, [append (Some a) y] is [Some
+    a], [append None (Some b)] is [Some b], and [append None None] is
+    [None]. *)
+val append : 'a option -> 'a option -> 'a option
+
 
 (** {6 "Iterators"} ***)
 
-- 
cgit v1.2.3