3 files changed, 4 insertions, 9 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index e9506803df..43807c1ca6 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -14,7 +14,7 @@ open Vernac
 open Pcoq
 
 let top_stderr x =
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ~pp_tag:Ppstyle.to_format) x
+  Format.fprintf !Topfmt.err_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. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 823d05580b..268d40c91d 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -311,18 +311,13 @@ let print_style_tags () =
   let tags = Ppstyle.dump () in
   let iter (t, st) =
     let st = match st with Some st -> st | None -> Terminal.make () in
-    let opt =
-      Terminal.eval st ^
-      String.concat "." (Ppstyle.repr t) ^
-      Terminal.reset ^ "\n"
-    in
+    let opt = Terminal.eval st ^ t ^   Terminal.reset ^ "\n" in
     print_string opt
   in
   let make (t, st) = match st with
   | None -> None
   | Some st ->
     let tags = List.map string_of_int (Terminal.repr st) in
-    let t = String.concat "." (Ppstyle.repr t) in
     Some (t ^ "=" ^ String.concat ";" tags)
   in
   let repr = List.map_filter make tags in
@@ -445,7 +440,7 @@ let get_native_name s =
     with the appropriate error code *)
 let fatal_error info anomaly =
   let msg = info ++ fnl () in
-  Format.fprintf !Topfmt.err_ft "@[%a@]%!" (pp_with ?pp_tag:None) msg;
+  Format.fprintf !Topfmt.err_ft "@[%a@]%!" pp_with msg;
   exit (if anomaly then 129 else 1)
 
 let parse_args arglist =
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 4fc4540c1c..06908abb6e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -181,7 +181,7 @@ let pp_cmd_header loc com =
  *)
 (* FIXME *)
 let print_cmd_header loc com =
-  Pp.pp_with ~pp_tag:Ppstyle.to_format !Topfmt.std_ft (pp_cmd_header loc com);
+  Pp.pp_with !Topfmt.std_ft (pp_cmd_header loc com);
   Format.pp_print_flush !Topfmt.std_ft ()
 
 let rec interp_vernac po chan_beautify checknav (loc,com) =