Getting rid of Pp.msg

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15400 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 19 insertions, 19 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 7434f5e8a..699f1f3df 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -696,14 +696,15 @@ type explanation =
 let check_disequalities state =
   let uf=state.uf in
   let rec check_aux = function
-      dis::q ->
-	debug (fun () -> msg
-	(str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
-	 pr_idx_term state dis.rhs ++ str " ... ")) ();
-	if find uf dis.lhs=find uf dis.rhs then
-	  begin debug msgnl (str "Yes");Some dis end
-	else
-	  begin debug msgnl (str "No");check_aux q end
+    | dis::q ->
+        let (info, ans) =
+          if find uf dis.lhs = find uf dis.rhs then (str "Yes", Some dis)
+          else (str "No", check_aux q)
+        in
+        let _ = debug (fun () -> msg_debug
+        (str "Checking if " ++ pr_idx_term state dis.lhs ++ str " = " ++
+         pr_idx_term state dis.rhs ++ str " ... " ++ info)) () in
+        ans
     | [] -> None
   in
     check_aux state.diseq
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 4438c5897..fe86e1ae1 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -99,7 +99,7 @@ END
 
 VERNAC COMMAND EXTEND PrintExtractionInline
 | [ "Print" "Extraction" "Inline" ]
-  -> [ print_extraction_inline () ]
+  -> [ msg_info (print_extraction_inline ()) ]
 END
 
 VERNAC COMMAND EXTEND ResetExtractionInline
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ecedc9002..0efdbbb6b 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -606,7 +606,6 @@ let extraction_inline b l =
 let print_extraction_inline () =
   let (i,n)= !inline_table in
   let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
-  msg
     (str "Extraction Inline:" ++ fnl () ++
      Refset'.fold
        (fun r p ->
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 7505664a6..978760e8e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -177,7 +177,7 @@ val find_custom_match : ml_branch array -> string
 
 val extraction_language : lang -> unit
 val extraction_inline : bool -> reference list -> unit
-val print_extraction_inline : unit -> unit
+val print_extraction_inline : unit -> Pp.std_ppcmds
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index d1fc8ef33..a169c2826 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -16,10 +16,10 @@ let observe strm =
   if do_observe ()
   then Pp.msgnl strm
   else ()
-let observennl strm =
+(*let observennl strm =
   if do_observe ()
   then Pp.msg strm
-  else ()
+  else ()*)
 
 
 type binder_type =
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b0897c61e..b463b6c27 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -55,10 +55,10 @@ let observe strm =
   then Pp.msgnl strm
   else ()
 
-let observennl strm =
+(*let observennl strm =
   if do_observe ()
   then begin Pp.msg strm;Pp.pp_flush () end
-  else ()
+  else ()*)
 
 
 let do_observe_tac s tac g =
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index d772279f1..a1ab6cd30 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -472,7 +472,7 @@ and pp_atom= function
   | Atom n -> int n
   | f -> str "(" ++ hv 2 (pp_form f) ++ str ")"
 
-let pr_form f = msg (pp_form f)
+let pr_form f = pp_form f
 
 let pp_intmap map =
   let pp=ref (str "") in
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index 275e94cde..738f3f230 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_search.mli
@@ -40,7 +40,7 @@ val success: state -> bool
 
 val pp: state -> Pp.std_ppcmds
 
-val pr_form : form -> unit
+val pr_form : form -> Pp.std_ppcmds
 
 val reset_info : unit -> unit
 
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 783aebafd..a095c545f 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -128,10 +128,10 @@ TACTIC EXTEND closed_term
 END
 ;;
 
-TACTIC EXTEND echo
+(* TACTIC EXTEND echo
 | [ "echo" constr(t) ] ->
   [ Pp.msg (Termops.print_constr t);  Tacinterp.eval_tactic (TacId []) ]
-END;;
+END;;*)
 
 (*
 let closed_term_ast l =