diff options
| -rw-r--r-- | tactics/auto.ml | 8 | ||||
| -rw-r--r-- | tactics/eauto.ml | 6 |
2 files changed, 7 insertions, 7 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 0f5b74d9d..6c5ecac94 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -260,19 +260,19 @@ let pr_info_atom (d,pp) = let pr_info_trace = function | (Info,_,{contents=(d,Some pp)::l}) -> - Feedback.msg_debug (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) + Feedback.msg_info (prlist_with_sep fnl pr_info_atom (cleanup_info_trace d [(d,pp)] l)) | _ -> () let pr_info_nop = function - | (Info,_,_) -> Feedback.msg_debug (str "idtac.") + | (Info,_,_) -> Feedback.msg_info (str "idtac.") | _ -> () let pr_dbg_header = function | (Off,_,_) -> () | (Debug,0,_) -> Feedback.msg_debug (str "(* debug trivial: *)") | (Debug,_,_) -> Feedback.msg_debug (str "(* debug auto: *)") - | (Info,0,_) -> Feedback.msg_debug (str "(* info trivial: *)") - | (Info,_,_) -> Feedback.msg_debug (str "(* info auto: *)") + | (Info,0,_) -> Feedback.msg_info (str "(* info trivial: *)") + | (Info,_,_) -> Feedback.msg_info (str "(* info auto: *)") let tclTRY_dbg d tac = let delay f = Proofview.tclUNIT () >>= fun () -> f () in 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) |