michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

feat(library/error_handling): improve unifier_exception error message

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 08:49:50 -07:00
parent e735a8e5ff
commit 6085a54416
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/error_handling/error_handling.cpp
View file

@ -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 {