From cf55a1bcc2f325a0dbbc72a12c061dc50b4a67a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 14 May 2014 10:35:42 -0700 Subject: [PATCH] fix(kernel/type_checker): typo 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 ad76738dde..b84b5142e4 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -209,7 +209,7 @@ struct type_checker::imp { expr A_args = mk_app(A, args.size(), args.data()); args.push_back(Var(0)); expr B_args = mk_app(B, args.size(), args.data()); - expr r = mk_pi(g_x_name, A, B); + expr r = mk_pi(g_x_name, A_args, B_args); justification j = mk_justification(s, [=](formatter const & fmt, options const & o, substitution const & subst) { return pp_function_expected(fmt, m_env, o, subst.instantiate_metavars_wo_jst(s));