From 65eea15cc3ec4b8316698db10ed02526a7dae4d0 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 28 Jun 2012 13:04:41 +0000
Subject: Fixing previous commit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15498 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/auto.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'tactics/auto.ml')

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 812ebd206..3b86d8262 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1226,13 +1226,14 @@ let pr_dbg_header = function
   | (Info,_,_) -> str "(* info auto : *)"
 
 let tclTRY_dbg d tac =
+  let (level, _, _) = d in
   tclORELSE0
     (fun gl ->
       let out = tac gl in
-      msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d);
+      if level <> Off then msg_debug (pr_dbg_header d ++ fnl () ++ pr_info_trace d);
       out)
     (fun gl ->
-      msg_debug (pr_info_nop d);
+      if level = Info then msg_debug (pr_info_nop d);
       tclIDTAC gl)
 
 (**************************************************************************)
-- 
cgit v1.2.3