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.

2 files changed, 14 insertions, 0 deletions

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"} ***)