Fix coq/ltac2#27: ... is not a particularly helpful printing of an error message.

1 files changed, 2 insertions, 1 deletions

diff --git a/src/tac2print.ml b/src/tac2print.ml
index fd1d759cce..ee45b33706 100644
--- a/src/tac2print.ml
+++ b/src/tac2print.ml
@@ -412,6 +412,7 @@ let () = register_init "message" begin fun pp ->
 end
 
 let () = register_init "err" begin fun e ->
-  let (e, _) = to_ext val_exn e in
+  let e = to_ext val_exn e in
+  let (e, _) = ExplainErr.process_vernac_interp_error ~allow_uncaught:true e in
   str "err:(" ++ CErrors.print_no_report e ++ str ")"
 end