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 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'lib/option.ml')

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
-- 
cgit v1.2.3