From c7b407cfd01495cd6ca37a7da9f2f5f2ddd3e75f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Feb 2017 11:17:18 -0800 Subject: [PATCH] fix(frontends/lean/elaborator): remove dirty trick used when generating type mismatch error messages, the trick was incompatible with the new error recovery code closes #1363 --- src/frontends/lean/elaborator.cpp | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a863cc5544..81003830ee 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1244,16 +1244,18 @@ expr elaborator::second_pass(expr const & fn, buffer const & args, expr new_arg_type = infer_type(new_arg); optional new_new_arg = ensure_has_type(new_arg, new_arg_type, info.args_expected_types[i], ref_arg); if (!new_new_arg) { - info.new_args.shrink(info.new_args_size[i]); - info.new_args.push_back(new_arg); - format msg = mk_app_type_mismatch_error(mk_app(fn, info.new_args.size(), info.new_args.data()), + buffer tmp_args; + tmp_args.append(info.new_args_size[i], info.new_args.data()); + tmp_args.push_back(new_arg); + format msg = mk_app_type_mismatch_error(mk_app(fn, tmp_args), new_arg, new_arg_type, info.args_expected_types[i]); throw elaborator_exception(ref, msg); } if (!is_def_eq(info.args_mvars[i], *new_new_arg)) { - info.new_args.shrink(info.new_args_size[i]); - info.new_args.push_back(new_arg); - format msg = mk_app_arg_mismatch_error(mk_app(fn, info.new_args.size(), info.new_args.data()), + buffer tmp_args; + tmp_args.append(info.new_args_size[i], info.new_args.data()); + tmp_args.push_back(new_arg); + format msg = mk_app_arg_mismatch_error(mk_app(fn, tmp_args), new_arg, info.args_mvars[i]); throw elaborator_exception(ref, msg); }