3 files changed, 26 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"} ***)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index af7d2a7232..ae7f2b1184 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -800,12 +800,24 @@ let command_focus = Proof.new_focus_kind ()
 let focus_command_cond = Proof.no_cond command_focus
 
 
+let print_info_trace = ref None
+
+let _ = let open Goptions in declare_int_option {
+  optsync = true;
+  optdepr = false;
+  optname = "print info trace";
+  optkey = ["Info" ; "Level"];
+  optread = (fun () -> !print_info_trace);
+  optwrite = fun n -> print_info_trace := n;
+}
+
 let vernac_solve n info tcom b =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode.";
   let status = Proof_global.with_current_proof (fun etac p ->
     let with_end_tac = if b then Some etac else None in
     let global = match n with SelectAll -> true | _ -> false in
+    let info = Option.append info !print_info_trace in
     let (p,status) =
       solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
     in