diff options
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index f0f408c24..2cae9b794 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -344,13 +344,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> msg_debug (str "idtac.") + | Info -> Feedback.msg_debug (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () - | Debug -> msg_debug (str "(* debug eauto : *)") - | Info -> msg_debug (str "(* info eauto : *)") + | Debug -> Feedback.msg_debug (str "(* debug eauto : *)") + | Info -> Feedback.msg_debug (str "(* info eauto : *)") let pr_info dbg s = if dbg != Info then () @@ -361,7 +361,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) |