diff options
| -rw-r--r-- | src/tac2print.ml | 3 |
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 |