diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-17 19:33:56 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-26 19:31:30 +0200 |
| commit | d500a684be14b0c781ea4cda0ee02d3c5cdcad81 (patch) | |
| tree | c29675a70ed7b67dfaca2766cf24be75eb121186 /tactics/eauto.ml | |
| parent | ff0fea7a07d85342586f65d68e9fdee0ff0c3d74 (diff) | |
Using msg_info for info_auto and info_eauto (PR #324).
Diffstat (limited to 'tactics/eauto.ml')
| -rw-r--r-- | tactics/eauto.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index c6d244867..5ca68cbe9 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -346,13 +346,13 @@ let mk_eauto_dbg d = else Off let pr_info_nop = function - | Info -> Feedback.msg_debug (str "idtac.") + | Info -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function | Off -> () | Debug -> Feedback.msg_debug (str "(* debug eauto: *)") - | Info -> Feedback.msg_debug (str "(* info eauto: *)") + | Info -> Feedback.msg_info (str "(* info eauto: *)") let pr_info dbg s = if dbg != Info then () @@ -363,7 +363,7 @@ let pr_info dbg s = | State sp -> let mindepth = loop sp in let indent = String.make (mindepth - sp.depth) ' ' in - Feedback.msg_debug (str indent ++ Lazy.force s.last_tactic ++ str "."); + Feedback.msg_info (str indent ++ Lazy.force s.last_tactic ++ str "."); mindepth in ignore (loop s) |