diff options
| author | Pierre-Marie Pédrot | 2016-05-31 14:26:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-31 14:26:27 +0200 |
| commit | 842dfef1d52c739119808ea1dec3509c0cf86435 (patch) | |
| tree | 072d78acd19daa086183b2431220e3701836ce56 /plugins/rtauto | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff) | |
| parent | 91ee24b4a7843793a84950379277d92992ba1651 (diff) | |
This patch splits pretty printing representation from IO operations.
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 3ba92b9f22..f3eae5f501 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 73dc13e72e..0a0b459156 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 |