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/auto.ml | |
| parent | ff0fea7a07d85342586f65d68e9fdee0ff0c3d74 (diff) | |
Using msg_info for info_auto and info_eauto (PR #324).
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 8 |
1 files changed, 4 insertions, 4 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 |