diff options
| -rw-r--r-- | tactics/auto.ml | 5 |
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) (**************************************************************************) |