diff options
Diffstat (limited to 'plugins/rtauto')
| -rw-r--r-- | plugins/rtauto/proof_search.ml | 2 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 12 |
2 files changed, 7 insertions, 7 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 3ba92b9f2..f3eae5f50 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -547,7 +547,7 @@ let pp_info () = int s_info.created_branches ++ str " created" ++ fnl () ++ str "Hypotheses : " ++ int s_info.created_hyps ++ str " created" ++ fnl () in - msg_info + Feedback.msg_info ( str "Proof-search statistics :" ++ fnl () ++ count_info ++ str "Branch ends: " ++ diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 73dc13e72..0a0b45915 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -276,7 +276,7 @@ let rtauto_tac gls= begin reset_info (); if !verbose then - msg_info (str "Starting proof-search ..."); + Feedback.msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in let prf = @@ -286,10 +286,10 @@ let rtauto_tac gls= let search_end_time = System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof tree found in " ++ + Feedback.msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); pp_info (); - msg_info (str "Building proof term ... ") + Feedback.msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in @@ -302,7 +302,7 @@ let rtauto_tac gls= let build_end_time=System.get_time () in let _ = if !verbose then begin - msg_info (str "Proof term built in " ++ + Feedback.msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ fnl () ++ str "Proof size : " ++ int !step_count ++ @@ -319,9 +319,9 @@ let rtauto_tac gls= Proofview.V82.of_tactic (Tactics.exact_no_check term) gls in let tac_end_time = System.get_time () in let _ = - if !check then msg_info (str "Proof term type-checking is on"); + if !check then Feedback.msg_info (str "Proof term type-checking is on"); if !verbose then - msg_info (str "Internal tactic executed in " ++ + Feedback.msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result |