From 120d3b5c1a68cb2dc076126f86519c3f84f0f833 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Jul 2014 19:38:20 +0100 Subject: [PATCH] fix(kernel/type_checker): error message 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 d4a566b8e..f9a657089 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -275,7 +275,7 @@ expr type_checker::infer_pi(expr const & _e, bool infer_only) { } expr type_checker::infer_app(expr const & e, bool infer_only) { - expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), app_fn(e)); + expr f_type = ensure_pi_core(infer_type_core(app_fn(e), infer_only), e); if (!infer_only) { expr a_type = infer_type_core(app_arg(e), infer_only); app_delayed_justification jst(e, f_type, a_type);