From 6085a54416ec4f57910bad36725bee1de30cf0f4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 08:49:50 -0700 Subject: [PATCH] feat(library/error_handling): improve unifier_exception error message Signed-off-by: Leonardo de Moura --- src/library/error_handling/error_handling.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 145e79d75..5f99831d7 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -53,7 +53,8 @@ static void display_error(io_state_stream const & ios, pos_info_provider const * formatter fmt = ios.get_formatter(); options opts = ios.get_options(); auto j = ex.get_justification(); - ios << mk_pair(j.pp(fmt, opts, p, ex.get_substitution()), opts) << endl; + display_error_pos(ios, p, j.get_main_expr()); + ios << " " << mk_pair(j.pp(fmt, opts, p, ex.get_substitution()), opts) << endl; } // struct delta_pos_info_provider : public pos_info_provider {