From 2b66bf0083fd85cf2fc983dbca75b848194f897f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 8 Sep 2017 02:32:54 +0200
Subject: Fix coq/ltac2#27: ... is not a particularly helpful printing of an
 error message.

---
 src/tac2print.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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
-- 
cgit v1.2.3