Fixing previous commit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15498 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 2 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 812ebd2064..3b86d82621 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)
 
 (**************************************************************************)