[pp] [ide] Minor cleanups in pp code.

- We avoid unnecessary use of Pp -> string conversion functions.
  and the creation of intermediate buffers on logging.

- We rename local functions that share the name with the Coq stdlib,
  this is usually dangerous as if the normal function is removed, code
  may pick up the one in the stdlib, with different semantics.

13 files changed, 81 insertions, 68 deletions

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index cee243f91..1b4c5d3be 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -128,6 +128,9 @@ end = struct
 end
 open SentenceId
 
+let log_pp msg : unit task =
+  Coq.lift (fun () -> Minilib.log_pp msg)
+
 let log msg : unit task =
   Coq.lift (fun () -> Minilib.log msg)
 
@@ -308,7 +311,7 @@ object(self)
 
   method private print_stack =
     Minilib.log "document:";
-    Minilib.log (Pp.string_of_ppcmds (Doc.print document (dbg_to_string buffer)))
+    Minilib.log_pp (Doc.print document (dbg_to_string buffer))
 
   method private enter_focus start stop =
     let at id id' _ = Stateid.equal id' id in
@@ -379,8 +382,7 @@ object(self)
     Coq.bind (Coq.seq action query) next
 
   method private mark_as_needed sentence =
-    Minilib.log("Marking " ^
-      Pp.string_of_ppcmds (dbg_to_string buffer false None sentence));
+    Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence);
     let start = buffer#get_iter_at_mark sentence.start in
     let stop = buffer#get_iter_at_mark sentence.stop in
     let to_process = Tags.Script.to_process in
@@ -437,9 +439,11 @@ object(self)
           | _ -> None in
         try Some (Doc.find_map document finder)
         with Not_found -> None in
-      let log s state_id =
-        Minilib.log ("Feedback " ^ s ^ " on " ^ Stateid.to_string
-          (Option.default Stateid.dummy state_id)) in
+      let log_pp s state_id =
+        Minilib.log_pp Pp.(seq
+                [str "Feedback "; s; str " on ";
+                 str (Stateid.to_string (Option.default Stateid.dummy state_id))]) in
+      let log s state_id = log_pp (Pp.str s) state_id in
       begin match msg.contents, sentence with
       | AddedAxiom, Some (id,sentence) ->
           log "AddedAxiom" id;
@@ -469,24 +473,24 @@ object(self)
             (Printf.sprintf "%s %s %s" filepath ident ty)
       | Message(Error, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let msg = Pp.string_of_ppcmds msg      in
-          log "ErrorMsg" id;
+          log_pp Pp.(str "ErrorMsg" ++ msg) id;
           remove_flag sentence `PROCESSING;
-          add_flag sentence (`ERROR (loc, msg));
+          let rmsg = Pp.string_of_ppcmds msg     in
+          add_flag sentence (`ERROR (loc, rmsg));
           self#mark_as_needed sentence;
-          self#attach_tooltip sentence loc msg;
+          self#attach_tooltip sentence loc rmsg;
           if not (Loc.is_ghost loc) then
             self#position_error_tag_at_sentence sentence (Some (Loc.unloc loc))
       | Message(Warning, loc, msg), Some (id,sentence) ->
           let loc = Option.default Loc.ghost loc in
-          let rmsg = Pp.string_of_ppcmds msg      in
-          log ("WarningMsg: " ^ Pp.string_of_ppcmds msg)id;
+          log_pp Pp.(str "WarningMsg" ++ msg) id;
+          let rmsg = Pp.string_of_ppcmds msg     in
           add_flag sentence (`WARNING (loc, rmsg));
           self#attach_tooltip sentence loc rmsg;
           self#position_warning_tag_at_sentence sentence loc;
           messages#push Warning msg
       | Message(lvl, loc, msg), Some (id,sentence) ->
-          log ("Msg: " ^ Pp.string_of_ppcmds msg) id;
+          log_pp Pp.(str "Msg" ++ msg) id;
           messages#push lvl msg
       | InProgress n, _ ->
           if n < 0 then processed <- processed + abs n
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 101f1a5ee..da867e689 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -337,7 +337,7 @@ let default_logger level message =
   | Feedback.Warning -> `WARNING
   | Feedback.Error -> `ERROR
   in
-  Minilib.log ~level (Pp.string_of_ppcmds message)
+  Minilib.log_pp ~level message
 
 
 (** {6 File operations} *)
diff --git a/ide/minilib.ml b/ide/minilib.ml
index d11e8c56b..2c24e46f8 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -30,7 +30,7 @@ let debug = ref false
    print in the response buffer.
 *)
 
-let log ?(level = `DEBUG) msg =
+let log_pp ?(level = `DEBUG) msg =
   let prefix = match level with
   | `DEBUG -> "DEBUG"
   | `INFO -> "INFO"
@@ -40,10 +40,12 @@ let log ?(level = `DEBUG) msg =
   | `FATAL -> "FATAL"
   in
   if !debug then begin
-    try Printf.eprintf "[%s] %s\n%!" prefix msg
+    try Format.eprintf "[%s] @[%a@]\n%!" prefix Pp.pp_with msg
     with _ -> ()
   end
 
+let log ?level str = log_pp ?level (Pp.str str)
+
 let coqify d = Filename.concat d "coq"
 
 let coqide_config_home () =
diff --git a/ide/minilib.mli b/ide/minilib.mli
index b7672c900..4517a2374 100644
--- a/ide/minilib.mli
+++ b/ide/minilib.mli
@@ -22,7 +22,8 @@ type level = [
 (** debug printing *)
 val debug : bool ref
 
-val log : ?level:level -> string -> unit
+val log_pp : ?level:level -> Pp.std_ppcmds -> unit
+val log    : ?level:level -> string        -> unit
 
 val coqide_config_home : unit -> string
 val coqide_config_dirs : unit -> string list
diff --git a/lib/pp.ml b/lib/pp.ml
index 7b21f9bbd..80c599274 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -77,6 +77,8 @@ let app s1 s2 = match s1, s2 with
   | s, Ppcmd_empty -> s
   | s1, s2         -> Ppcmd_glue [s1; s2]
 
+let seq s = Ppcmd_glue s
+
 let (++) = app
 
 (* formatting commands *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 2c45ce0a7..4b7ac5c1a 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -68,6 +68,9 @@ val comment  : string list -> std_ppcmds
 val app : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Concatenation. *)
 
+val seq : std_ppcmds list -> std_ppcmds
+(** Multi-Concatenation. *)
+
 val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
 (** Infix alias for [app]. *)
 
diff --git a/library/summary.ml b/library/summary.ml
index 6efa07f38..2ec4760d6 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -107,8 +107,10 @@ let unfreeze_summaries fs =
     try fold id decl state
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
-      Printf.eprintf "Error unfrezing summay %s\n%s\n%!"
-        (name_of_summary id) (Pp.string_of_ppcmds (CErrors.iprint e));
+      Feedback.msg_error
+        Pp.(seq [str "Error unfrezing summay %s\n%s\n%!";
+                 str (name_of_summary id);
+                 CErrors.iprint e]);
       iraise e
   in
   (** We rely on the order of the frozen list, and the order of folding *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 120cde5e5..ca7330fdb 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -195,9 +195,9 @@ let check_no_pending_proof () =
   if not (there_are_pending_proofs ()) then
     ()
   else begin
-    CErrors.error (Pp.string_of_ppcmds
+    CErrors.user_err
       (str"Proof editing in progress" ++ msg_proofs () ++ fnl() ++
-       str"Use \"Abort All\" first or complete proof(s)."))
+       str"Use \"Abort All\" first or complete proof(s).")
   end
 
 let discard_gen id =
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
index a125fb10d..f51586c73 100644
--- a/proofs/proof_using.ml
+++ b/proofs/proof_using.ml
@@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids =
 let suggest_Proof_using name env vars ids_typ context_ids =
   let module S = Id.Set in
   let open Pp in
-  let print x = prerr_endline (string_of_ppcmds x) in
+  let print x = Feedback.msg_error x in
   let pr_set parens s =
     let wrap ppcmds =
       if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 28548ecee..125491988 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -10,9 +10,9 @@ open CErrors
 open Pp
 open Util
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err pp = Format.eprintf "%s] @[%a@]%!\n" (System.process_id ()) Pp.pp_with pp
 
-let prerr_endline s = if !Flags.debug then begin pr_err s end else ()
+let stm_prerr_endline s = if !Flags.debug then begin stm_pr_err (str s) end else ()
 
 type 'a worker_status = [ `Fresh | `Old of 'a ]
 
@@ -147,23 +147,23 @@ module Make(T : Task) = struct
     let stop_waiting = ref false in
     let expiration_date = ref (ref false) in
     let pick_task () =
-      prerr_endline "waiting for a task";
+      stm_prerr_endline "waiting for a task";
       let pick age (t, c) = not !c && T.task_match age t in
       let task, task_expiration =
         TQueue.pop ~picky:(pick !worker_age) ~destroy:stop_waiting queue in
       expiration_date := task_expiration;
       last_task := Some task;
-      prerr_endline ("got task: "^T.name_of_task task);
+      stm_prerr_endline ("got task: " ^ T.name_of_task task);
       task in
     let add_tasks l =
       List.iter (fun t -> TQueue.push queue (t,!expiration_date)) l in
     let get_exec_token () =
       ignore(CoqworkmgrApi.get 1);
       got_token := true;
-      prerr_endline ("got execution token") in
+      stm_prerr_endline ("got execution token") in
     let kill proc =
       Worker.kill proc;
-      prerr_endline ("Worker exited: " ^
+      stm_prerr_endline ("Worker exited: " ^
         match Worker.wait proc with
         | Unix.WEXITED 0x400 -> "exit code unavailable"
         | Unix.WEXITED i -> Printf.sprintf "exit(%d)" i
@@ -196,7 +196,7 @@ module Make(T : Task) = struct
       report_status ~id "Idle";
       let task = pick_task () in
       match T.request_of_task !worker_age task with
-      | None -> prerr_endline ("Task expired: " ^ T.name_of_task task)
+      | None -> stm_prerr_endline ("Task expired: " ^ T.name_of_task task)
       | Some req ->
       try
         get_exec_token ();
@@ -222,8 +222,7 @@ module Make(T : Task) = struct
           raise e (* we pass the exception to the external handler *)
       | MarshalError s -> T.on_marshal_error s task; raise Die
       | e ->
-          pr_err ("Uncaught exception in worker manager: "^
-            string_of_ppcmds (print e));
+          stm_pr_err Pp.(seq [str "Uncaught exception in worker manager: "; print e]);
           flush_all (); raise Die
     done with
     | (Die | TQueue.BeingDestroyed) ->
@@ -261,7 +260,7 @@ module Make(T : Task) = struct
   let broadcast { queue } = TQueue.broadcast queue
 
   let enqueue_task { queue; active } (t, _ as item) =
-    prerr_endline ("Enqueue task "^T.name_of_task t);
+    stm_prerr_endline ("Enqueue task "^T.name_of_task t);
     TQueue.push queue item
 
   let cancel_worker { active } n = Pool.cancel n active
@@ -329,11 +328,11 @@ module Make(T : Task) = struct
         CEphemeron.clear ()
       with
       | MarshalError s ->
-        pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
+        stm_pr_err Pp.(prlist str ["Fatal marshal error: "; s]); flush_all (); exit 2
       | End_of_file ->
-        prerr_endline "connection lost"; flush_all (); exit 2
+        stm_prerr_endline "connection lost"; flush_all (); exit 2
       | e ->
-        pr_err ("Slave: critical exception: " ^ Pp.string_of_ppcmds (print e));
+        stm_pr_err Pp.(seq [str "Slave: critical exception: "; print e]);
         flush_all (); exit 1
     done
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 75872d633..ee142b293 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -6,10 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-let pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
+let stm_pr_err s = Printf.eprintf "%s] %s\n" (System.process_id ()) s; flush stderr
 
-let prerr_endline s = if false then begin pr_err (s ()) end else ()
-let prerr_debug s = if !Flags.debug then begin pr_err (s ()) end else ()
+let stm_prerr_endline s = if false then begin stm_pr_err (s ()) end else ()
+let stm_prerr_debug s = if !Flags.debug then begin stm_pr_err (s ()) end else ()
 
 open Vernacexpr
 open CErrors
@@ -540,7 +540,7 @@ end = struct (* {{{ *)
         let branch, mode = match Vcs_aux.find_proof_at_depth !vcs pl with
           | h, { Vcs_.kind = `Proof (m, _) } -> h, m | _ -> assert false in
         checkout branch;
-        prerr_endline (fun () -> "mode:" ^ mode);
+        stm_prerr_endline (fun () -> "mode:" ^ mode);
         Proof_global.activate_proof_mode mode
       with Failure _ ->
         checkout Branch.master;
@@ -852,7 +852,7 @@ end = struct (* {{{ *)
     if is_cached id && not redefine then
       anomaly (str"defining state "++str str_id++str" twice");
     try
-      prerr_endline (fun () -> "defining "^str_id^" (cache="^
+      stm_prerr_endline (fun () -> "defining "^str_id^" (cache="^
         if cache = `Yes then "Y)" else if cache = `Shallow then "S)" else "N)");
       let good_id = match safe_id with None -> !cur_id | Some id -> id in
       fix_exn_ref := exn_on id ~valid:good_id;
@@ -860,7 +860,7 @@ end = struct (* {{{ *)
       fix_exn_ref := (fun x -> x);
       if cache = `Yes then freeze `No id
       else if cache = `Shallow then freeze `Shallow id;
-      prerr_endline (fun () -> "setting cur id to "^str_id);
+      stm_prerr_endline (fun () -> "setting cur id to "^str_id);
       cur_id := id;
       if feedback_processed then
         Hooks.(call state_computed id ~in_cache:false);
@@ -994,11 +994,11 @@ let stm_vernac_interp ?proof id ?route { verbose; loc; expr } =
   in
   let aux_interp cmd =
   if is_filtered_command cmd then
-    prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
+    stm_prerr_endline (fun () -> "ignoring " ^ Pp.string_of_ppcmds(pr_vernac expr))
   else match cmd with
   | VernacShow ShowScript -> ShowScript.show_script ()
   | expr ->
-    prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
+    stm_prerr_endline (fun () -> "interpreting " ^ Pp.string_of_ppcmds(pr_vernac expr));
     try Vernacentries.interp ?verbosely:(Some verbose) ?proof (loc, expr)
     with e ->
       let e = CErrors.push e in
@@ -1431,8 +1431,8 @@ end = struct (* {{{ *)
           | Some (safe, err) -> err, safe
           | None -> Stateid.dummy, Stateid.dummy in
         let e_msg = iprint (e, info) in
-        prerr_endline (fun () -> "failed with the following exception:");
-        prerr_endline (fun () -> string_of_ppcmds e_msg);
+        stm_prerr_endline (fun () -> "failed with the following exception:");
+        stm_prerr_endline (fun () -> string_of_ppcmds e_msg);
         let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
   
@@ -1697,7 +1697,7 @@ end = struct (* {{{ *)
              | Some (ReqBuildProof (r, b, _)) -> Some(r, b)
              | _ -> None)
         tasks in
-    prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
+    stm_prerr_endline (fun () -> Printf.sprintf "dumping %d tasks\n" (List.length reqs));
     reqs
 
   let reset_task_queue () = TaskQueue.clear (Option.get !queue)
@@ -1781,7 +1781,7 @@ end = struct (* {{{ *)
         `Stay ((),[])
                     
   let on_marshal_error err { t_name } =
-    pr_err ("Fatal marshal error: " ^ t_name );
+    stm_pr_err ("Fatal marshal error: " ^ t_name );
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death = function
@@ -1880,7 +1880,7 @@ end = struct (* {{{ *)
           let open Notations in
           try
             let pt, uc = Future.join f in
-            prerr_endline (fun () -> string_of_ppcmds(hov 0 (
+            stm_prerr_endline (fun () -> string_of_ppcmds(hov 0 (
               str"g=" ++ int (Evar.repr gid) ++ spc () ++
               str"t=" ++ (Printer.pr_constr pt) ++ spc () ++
               str"uc=" ++ Evd.pr_evar_universe_context uc)));
@@ -1925,7 +1925,7 @@ end = struct (* {{{ *)
   let use_response _ _ _ = `End
 
   let on_marshal_error _ _ =
-    pr_err ("Fatal marshal error in query");
+    stm_pr_err ("Fatal marshal error in query");
     flush_all (); exit 1
 
   let on_task_cancellation_or_expiration_or_slave_death _ = ()
@@ -2000,7 +2000,7 @@ let warn_deprecated_nested_proofs =
                     "stop working in a future Coq version"))
 
 let collect_proof keep cur hd brkind id =
- prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
+ stm_prerr_endline (fun () -> "Collecting proof ending at "^Stateid.to_string id);
  let no_name = "" in
  let name = function
    | [] -> no_name
@@ -2100,7 +2100,7 @@ let string_of_reason = function
   | `NoPU_NoHint_NoES -> "no 'Proof using..', no .aux file, inside a section"
   | `Unknown -> "unsupported case"
 
-let log_string s = prerr_debug (fun () -> "STM: " ^ s)
+let log_string s = stm_prerr_debug (fun () -> "STM: " ^ s)
 let log_processing_async id name = log_string Printf.(sprintf
   "%s: proof %s: asynch" (Stateid.to_string id) name
 )
@@ -2187,16 +2187,16 @@ let known_state ?(redefine_qed=false) ~cache id =
     Summary.unfreeze_summary s; Lib.unfreeze l; update_global_env ()
   in
   let rec pure_cherry_pick_non_pstate safe_id id = Future.purify (fun id ->
-    prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
+    stm_prerr_endline (fun () -> "cherry-pick non pstate " ^ Stateid.to_string id);
     reach ~safe_id id;
     cherry_pick_non_pstate ()) id
 
   (* traverses the dag backward from nodes being already calculated *)
   and reach ?safe_id ?(redefine_qed=false) ?(cache=cache) id =
-    prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
+    stm_prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
       Hooks.(call state_computed id ~in_cache:true);
-      prerr_endline (fun () -> "reached (cache)");
+      stm_prerr_endline (fun () -> "reached (cache)");
       State.install_cached id
     end else
     let step, cache_step, feedback_processed =
@@ -2348,7 +2348,7 @@ let known_state ?(redefine_qed=false) ~cache id =
       else cache_step in
     State.define ?safe_id
       ~cache:cache_step ~redefine:redefine_qed ~feedback_processed step id;
-    prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
+    stm_prerr_endline (fun () -> "reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
 end (* }}} *)
@@ -2363,7 +2363,7 @@ let init () =
   Backtrack.record ();
   Slaves.init ();
   if Flags.async_proofs_is_master () then begin
-    prerr_endline (fun () -> "Initializing workers");
+    stm_prerr_endline (fun () -> "Initializing workers");
     Query.init ();
     let opts = match !Flags.async_proofs_private_flags with
       | None -> []
@@ -2415,9 +2415,9 @@ let rec join_admitted_proofs id =
 let join () =
   finish ();
   wait ();
-  prerr_endline (fun () -> "Joining the environment");
+  stm_prerr_endline (fun () -> "Joining the environment");
   Global.join_safe_environment ();
-  prerr_endline (fun () -> "Joining Admitted proofs");
+  stm_prerr_endline (fun () -> "Joining Admitted proofs");
   join_admitted_proofs (VCS.get_branch_pos (VCS.current_branch ()));
   VCS.print ();
   VCS.print ()
@@ -2491,7 +2491,7 @@ let handle_failure (e, info) vcs tty =
       anomaly(str"error with no safe_id attached:" ++ spc() ++
         CErrors.iprint_no_report (e, info))
   | Some (safe_id, id) ->
-      prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+      stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
       VCS.restore vcs;
       if tty && interactive () = `Yes then begin
         (* We stay on a valid state *)
@@ -2514,13 +2514,13 @@ let reset_task_queue = Slaves.reset_task_queue
 (* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty
   ({ verbose; loc; expr } as x) c =
-  prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
+  stm_prerr_endline (fun () -> "{{{ processing: "^ string_of_ppcmds (pr_ast x));
   let vcs = VCS.backup () in
   try
     let head = VCS.current_branch () in
     VCS.checkout head;
     let rc = begin
-      prerr_endline (fun () ->
+      stm_prerr_endline (fun () ->
         "  classified as: " ^ string_of_vernac_classification c);
       match c with
       (* PG stuff *)    
@@ -2558,7 +2558,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
           VCS.commit id (Alias (oid,x));
           Backtrack.record (); if w == VtNow then finish (); `Ok
       | VtStm (VtBack id, false), VtNow ->
-          prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
+          stm_prerr_endline (fun () -> "undo to state " ^ Stateid.to_string id);
           Backtrack.backto id;
           VCS.checkout_shallowest_proof_branch ();
           Reach.known_state ~cache:(interactive ()) id; `Ok
@@ -2708,7 +2708,7 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty
               expr = VernacShow (ShowGoal OpenSubgoals) }
       | _ -> ()
     end;
-    prerr_endline (fun () -> "processed }}}");
+    stm_prerr_endline (fun () -> "processed }}}");
     VCS.print ();
     rc
   with e ->
@@ -2894,7 +2894,7 @@ let edit_at id =
         anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
           CErrors.print_no_report e)
     | Some (_, id) ->
-        prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
+        stm_prerr_endline (fun () -> "Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         iraise (e, info)
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 594f2e944..6d71601cc 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -444,14 +444,14 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
                with Not_found ->
 		 (* spiwack: the format of this error message should probably
 	                     be improved. *)
-		 let err_msg = string_of_ppcmds
+		 let err_msg =
 	                                (str "boolean->Leibniz:" ++
                                          str "You have to declare the" ++
 			   	         str "decidability over " ++
 				         Printer.pr_constr tt1 ++
 				         str " first.")
 		 in
-		 error err_msg
+		 user_err err_msg
                in let bl_args =
                         Array.append (Array.append
                           (Array.map (fun x -> x) v)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 09c43f93e..999fe297e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -39,7 +39,7 @@ module NamedDecl = Context.Named.Declaration
 let (f_interp_redexp, interp_redexp_hook) = Hook.make ()
 
 let debug = false
-let prerr_endline x =
+let vernac_prerr_endline x =
   if debug then prerr_endline (x ()) else ()
 
 (* Misc *)
@@ -1933,7 +1933,7 @@ let vernac_load interp fname =
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~loc locality poly c =
-  prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
+  vernac_prerr_endline (fun () -> "interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c));
   match c with
   (* The below vernac are candidates for removal from the main type
      and to be put into a new doc_command datatype: *)