diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index ec7672b90f8f..9f98d02403b1 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -15,6 +15,9 @@ let print_emacs = ref false
 let top_stderr x =
   Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with x
 
+let top_std x =
+  Format.fprintf !Topfmt.std_ft "@[%a@]%!" pp_with x
+
 (* A buffer for the character read from a channel. We store the command
  * entered to be able to report errors without pretty-printing. *)
 
@@ -59,7 +62,7 @@ let prompt_char doc ic ibuf count =
     | ll::_ -> Int.equal ibuf.len ll
     | [] -> Int.equal ibuf.len 0
   in
-  if bol && not !print_emacs then top_stderr (str (ibuf.prompt doc));
+  if bol && not !print_emacs then top_std (str (ibuf.prompt doc));
   try
     let c = input_char ic in
     if c == '\n' then ibuf.bols <- (ibuf.len+1) :: ibuf.bols;
@@ -331,9 +334,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in
 (* This mimics the semantics of the old Pp.flush_all *)
 let loop_flush_all () =
   flush stderr;
+  Format.pp_print_flush !Topfmt.err_ft ();
   flush stdout;
-  Format.pp_print_flush !Topfmt.std_ft ();
-  Format.pp_print_flush !Topfmt.err_ft ()
+  Format.pp_print_flush !Topfmt.std_ft ()
 
 (* Goal equality heuristic. *)
 let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2
@@ -495,7 +498,7 @@ let rec vernac_loop ~state =
   let open Vernac.State in
   loop_flush_all ();
   top_stderr (fnl());
-  if !print_emacs then top_stderr (str (top_buffer.prompt state.doc));
+  if !print_emacs then top_std (str (top_buffer.prompt state.doc));
   resynch_buffer top_buffer;
   let state, drop = read_and_execute ~state in
   if drop then state else (vernac_loop [@ocaml.tailcall]) ~state