From cf7660a3a8932ee593a376e8ec7ec251896a72e3 Mon Sep 17 00:00:00 2001
From: ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 1 Jun 2012 18:03:06 +0000
Subject: 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
---
 plugins/rtauto/proof_search.ml |  2 +-
 plugins/rtauto/refl_tauto.ml   | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index a1ab6cd30..46d561ed8 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -533,7 +533,7 @@ let pp_info () =
 	int s_info.created_branches ++ str " created" ++ fnl () ++
 	str "Hypotheses : " ++
 	int s_info.created_hyps ++ str " created" ++ fnl () in
-    msgnl
+    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 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
 
-- 
cgit v1.2.3