More cleaning

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

11 files changed, 25 insertions, 57 deletions

diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index 3a47ade0df..06c3ac3f94 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -54,9 +54,9 @@ let rec extract_signature = function
 let check_unicity s l =
   let l' = List.map (fun (l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
-    Pp.warning_with !Pp_control.err_ft
-      ("Two distinct rules of tactic entry "^s^" have the same\n"^
-      "non-terminals in the same order: put them in distinct tactic entries")
+    Pp.msg_warning
+      (strbrk ("Two distinct rules of tactic entry "^s^" have the same "^
+      "non-terminals in the same order: put them in distinct tactic entries"))
 
 let make_clause (pt,e) =
   (make_patt pt,
diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4
index af7ee7d169..b66460fe6f 100644
--- a/grammar/vernacextend.ml4
+++ b/grammar/vernacextend.ml4
@@ -31,9 +31,9 @@ let rec make_let e = function
 let check_unicity s l =
   let l' = List.map (fun (_,l,_) -> extract_signature l) l in
   if not (Util.list_distinct l') then
-    Pp.warning_with !Pp_control.err_ft
-      ("Two distinct rules of entry "^s^" have the same\n"^
-      "non-terminals in the same order: put them in distinct vernac entries")
+    Pp.msg_warning
+      (strbrk ("Two distinct rules of entry "^s^" have the same "^
+      "non-terminals in the same order: put them in distinct vernac entries"))
 
 let make_clause (_,pt,e) =
   (make_patt pt,
diff --git a/lib/pp.ml4 b/lib/pp.ml4
index 35621a5d7c..0ec4ea4c91 100644
--- a/lib/pp.ml4
+++ b/lib/pp.ml4
@@ -328,6 +328,7 @@ let flush_all() = flush stderr; flush stdout; pp_flush()
 let msg x = msg_with !std_ft x
 let msgnl x = msgnl_with !std_ft x
 let msg_info x = msgnl x
+let msg_tactic x = msgnl x
 let msgerr x = msg_with !err_ft x
 let msgerrnl x = msgnl_with !err_ft x
 let msg_warning x = msg_warning_with !err_ft x
diff --git a/lib/pp.mli b/lib/pp.mli
index e3a3535e91..58a5171d31 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -78,6 +78,7 @@ val tclose : unit -> std_ppcmds
 
 val msg_info : std_ppcmds -> unit
 val msg_warning : std_ppcmds -> unit
+(* val msg_tactic : std_ppcmds -> unit *)
 val msg_debug : std_ppcmds -> unit
 
 val string_of_ppcmds : std_ppcmds -> string
@@ -137,8 +138,6 @@ val surround : std_ppcmds -> std_ppcmds
 
 val pp_with : Format.formatter -> std_ppcmds -> unit
 val ppnl_with : Format.formatter -> std_ppcmds -> unit
-val warning_with : Format.formatter -> string -> unit
-val warn_with : Format.formatter -> std_ppcmds -> unit
 val pp_flush_with : Format.formatter -> unit -> unit
 
 (** {6 Pretty-printing functions {% \emph{%}without flush{% }%} on [stdout] and [stderr]. } *)
@@ -158,5 +157,4 @@ val set_warning_function : (Format.formatter -> std_ppcmds -> unit) -> unit
 (** {6 Low-level pretty-printing functions {% \emph{%}with flush{% }%}. } *)
 
 val msg_with : Format.formatter -> std_ppcmds -> unit
-val msgnl_with : Format.formatter -> std_ppcmds -> unit
 
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 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 84a1cd550f..bd47badfe3 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1679,7 +1679,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
         let ty = evi.evar_concl in
         Typing.check env evd' body ty
       with e ->
-        pperrnl
+        msg_info
           (str "Ill-typed evar instantiation: " ++ fnl() ++
            pr_evar_map evd' ++ fnl() ++
            str "----> " ++ int ev ++ str " := " ++
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 1cde368a11..cdc7fd73b5 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -142,14 +142,6 @@ and e_my_find_search db_list local_db hdc concl =
 	   | Extern tacast -> conclPattern concl p tacast
        in
        (tac,lazy (pr_autotactic t)))
-       (*i
-	 fun gls -> pPNL (pr_autotactic t); pp_flush ();
-                     try tac gls
-		     with e when Logic.catchable_exception(e) ->
-                            (str "Fail\n";
-			     pp_flush ();
-			     raise e)
-       i*)
   in
   List.map tac_of_hint hintl
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 485b46aef3..314d712dc0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1250,7 +1250,7 @@ let vernac_print = function
   | PrintUniverses (b, None) ->
     let univ = Global.universes () in
     let univ = if b then Univ.sort_universes univ else univ in
-    pp (Univ.pr_universes univ)
+    msg_info (Univ.pr_universes univ)
   | PrintUniverses (b, Some s) -> dump_universes b s
   | PrintHint r -> msg_info (Auto.pr_hint_ref (smart_global r))
   | PrintHintGoal -> msg_info (Auto.pr_applicable_hint ())
@@ -1258,11 +1258,11 @@ let vernac_print = function
   | PrintRewriteHintDbName s -> msg_info (Autorewrite.print_rewrite_hintdb s)
   | PrintHintDb -> msg_info (Auto.pr_searchtable ())
   | PrintScopes ->
-      pp (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
+      msg_info (Notation.pr_scopes (Constrextern.without_symbols pr_lglob_constr))
   | PrintScope s ->
-      pp (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_info (Notation.pr_scope (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintVisibility s ->
-      pp (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
+      msg_info (Notation.pr_visibility (Constrextern.without_symbols pr_lglob_constr) s)
   | PrintAbout qid -> msg_info (print_about qid)
   | PrintImplicit qid -> msg_info (print_impargs qid)
   | PrintAssumptions (o,r) ->