diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 18:03:06 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-01 18:03:06 +0000 |
| commit | cf7660a3a8932ee593a376e8ec7ec251896a72e3 (patch) | |
| tree | 5f3fd167f5dd704bf5482d236624aa8ef8bf6707 /plugins/rtauto/refl_tauto.ml | |
| parent | 35e4ac349af4fabbc5658b5cba632f98ec04da3f (diff) | |
Getting rid of Pp.msgnl and Pp.message.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15412 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/rtauto/refl_tauto.ml')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index 60ef81286..8db267641 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -285,7 +285,7 @@ let rtauto_tac gls= begin reset_info (); if !verbose then - msgnl (str "Starting proof-search ..."); + msg_info (str "Starting proof-search ..."); end in let search_start_time = System.get_time () in let prf = @@ -295,10 +295,10 @@ let rtauto_tac gls= let search_end_time = System.get_time () in let _ = if !verbose then begin - msgnl (str "Proof tree found in " ++ + msg_info (str "Proof tree found in " ++ System.fmt_time_difference search_start_time search_end_time); pp_info (); - msgnl (str "Building proof term ... ") + msg_info (str "Building proof term ... ") end in let build_start_time=System.get_time () in let _ = step_count := 0; node_count := 0 in @@ -311,7 +311,7 @@ let rtauto_tac gls= let build_end_time=System.get_time () in let _ = if !verbose then begin - msgnl (str "Proof term built in " ++ + msg_info (str "Proof term built in " ++ System.fmt_time_difference build_start_time build_end_time ++ fnl () ++ str "Proof size : " ++ int !step_count ++ @@ -328,9 +328,9 @@ let rtauto_tac gls= Tactics.exact_no_check term gls in let tac_end_time = System.get_time () in let _ = - if !check then msgnl (str "Proof term type-checking is on"); + if !check then msg_info (str "Proof term type-checking is on"); if !verbose then - msgnl (str "Internal tactic executed in " ++ + msg_info (str "Internal tactic executed in " ++ System.fmt_time_difference tac_start_time tac_end_time) in result |