From 8e402ae862881cd6f8c507626f32d59d17b35977 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 26 Jul 2014 20:33:44 -0700 Subject: [PATCH] fix(kernel/type_checker): error message position information Signed-off-by: Leonardo de Moura --- src/kernel/type_checker.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index b988236a3..dcafd9bfc 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -281,7 +281,7 @@ expr type_checker::infer_app(expr const & e, bool infer_only) { expr a_type = infer_type_core(app_arg(e), infer_only); app_delayed_justification jst(e, f_type, a_type); if (!is_def_eq(a_type, binding_domain(f_type), jst)) { - throw_kernel_exception(m_env, app_arg(e), + throw_kernel_exception(m_env, e, [=](formatter const & fmt) { return pp_app_type_mismatch(fmt, e, binding_domain(f_type), a_type); });