From 5c40b466ccfb2ec74c795a5f0751f962f4ad8f5e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 25 Jun 2014 10:42:58 -0700 Subject: [PATCH] fix(kernel/type_checker): use the application to provide error location 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 578d54257..b44023542 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -230,7 +230,7 @@ justification app_delayed_justification::get() { expr e = m_e; expr fn_type = m_fn_type; expr arg_type = m_arg_type; - m_jst = mk_justification(app_arg(e), + m_jst = mk_justification(e, [=](formatter const & fmt, options const & o, substitution const & subst) { return pp_app_type_mismatch(fmt, env, o, subst.instantiate_metavars_wo_jst(e),