More cleaning

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

4 files changed, 12 insertions, 35 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index f107007363..4aa6eaa1c5 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -465,7 +465,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
   (* First, a dry run, for computing objects to rename or duplicate *)
   set_phase Pre;
   let devnull = formatter true None in
-  msg_with devnull (d.pp_struct struc);
+  pp_with devnull (d.pp_struct struc);
   let opened = opened_libraries () in
   (* Print the implementation *)
   let cout = if dry then None else Option.map open_out fn in
@@ -473,8 +473,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
   begin try
     (* The real printing of the implementation *)
     set_phase Impl;
-    msg_with ft (d.preamble mo opened unsafe_needs);
-    msg_with ft (d.pp_struct struc);
+    pp_with ft (d.preamble mo opened unsafe_needs);
+    pp_with ft (d.pp_struct struc);
     Option.iter close_out cout;
   with e ->
     Option.iter close_out cout; raise e
@@ -487,8 +487,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
        let ft = formatter false (Some cout) in
        begin try
 	 set_phase Intf;
-	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
-	 msg_with ft (d.pp_sig (signature_of_structure struc));
+	 pp_with ft (d.sig_preamble mo opened unsafe_needs);
+	 pp_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
        with e ->
 	 close_out cout; raise e
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index bd5fd9c09c..b8887c68f9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -23,23 +23,15 @@ open Misctypes
 (*
 let observe strm =
   if do_observe ()
-  then Pp.msgnl strm
-  else ()
-
-let observennl strm =
-  if do_observe ()
-  then begin Pp.msg strm;Pp.pp_flush () end
+  then Pp.msg_debug strm
   else ()
 
-
-
-
 let do_observe_tac s tac g =
  try let v = tac g in (* msgnl (goal ++ fnl () ++ (str s)++(str " ")++(str "finished")); *) v
  with e ->
    let e = Cerrors.process_vernac_interp_error e in
    let goal = begin try (Printer.pr_goal g) with _ -> assert false end in
-   msgnl (str "observation "++ s++str " raised exception " ++
+   msg_debug (str "observation "++ s++str " raised exception " ++
 	    Errors.print e ++ str " on goal " ++ goal );
    raise e;;
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 7cf438e6f5..fe359f08d9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1366,7 +1366,6 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
     end;
   try
     by tclIDTAC; (* raises UserError _ if the proof is complete *)
-    if Flags.is_verbose () then (pp (Printer.pr_open_subgoals()))
   with UserError _ ->
     defined ()
 
@@ -1521,7 +1520,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
       with e ->
 	begin
 	  if do_observe ()
-	  then pperrnl (str "Cannot create equation Lemma " ++ Errors.print e)
+	  then msg_debug (str "Cannot create equation Lemma " ++ Errors.print e)
 	  else anomaly "Cannot create equation Lemma"
 	  ;
 	  true
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 10eaa98b30..68dc0319fa 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -16,6 +16,7 @@
 (*                                                                      *)
 (************************************************************************)
 
+open Pp
 open Mutils
 
 (**
@@ -894,10 +895,7 @@ struct
 
   let parse_expr parse_constant parse_exp ops_spec env term =
     if debug
-    then (Pp.pp (Pp.str "parse_expr: ");
-          Pp.pp (Printer.prterm term);
-          Pp.pp (Pp.str "\n");
-          Pp.pp_flush ());
+    then Pp.msg_debug (Pp.str "parse_expr: " ++ Printer.prterm term);
 
 (*
     let constant_or_variable env term =
@@ -1013,11 +1011,7 @@ struct
 
   let rconstant term = 
     if debug
-    then (Pp.pp_flush ();
-          Pp.pp (Pp.str "rconstant: ");
-          Pp.pp (Printer.prterm  term);
-          Pp.pp (Pp.str "\n");
-          Pp.pp_flush ());
+    then Pp.msg_debug (Pp.str "rconstant: " ++ Printer.prterm term ++ fnl ());
     let res = rconstant term in
       if debug then 
 	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
@@ -1057,11 +1051,7 @@ struct
 
   let  parse_arith parse_op parse_expr env cstr =
    if debug
-   then (Pp.pp_flush ();
-         Pp.pp (Pp.str "parse_arith: ");
-         Pp.pp (Printer.prterm  cstr);
-         Pp.pp (Pp.str "\n");
-         Pp.pp_flush ());
+   then Pp.msg_debug (Pp.str "parse_arith: " ++ Printer.prterm  cstr ++ fnl ());
    match kind_of_term cstr with
     | App(op,args) ->
        let (op,lhs,rhs) = parse_op (op,args) in
@@ -1645,8 +1635,6 @@ let micromega_gen
 		  (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
 	      ]) gl
   with
-(*   | Failure x -> flush stdout ; Pp.pp_flush () ;
-      Tacticals.tclFAIL 0 (Pp.str x) gl *)
    | ParseError  -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
    | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
       Tacticals.tclFAIL 0 (Pp.str 
@@ -1716,8 +1704,6 @@ let micromega_genr prover gl =
                 micromega_order_changer res' env (abstract_wrt_formula ff' ff)
               ]) gl
   with
-(*   | Failure x -> flush stdout ; Pp.pp_flush () ;
-      Tacticals.tclFAIL 0 (Pp.str x) gl *)
    | ParseError  -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
    | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
       Tacticals.tclFAIL 0 (Pp.str