From 1ee6bb48fc4f6e223ee70de81ee8d995b42eb746 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 25 May 2014 06:25:31 -0700 Subject: [PATCH] fix(library/coercion): bug in add_coercion_trans Signed-off-by: Leonardo de Moura --- src/library/coercion.cpp | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/src/library/coercion.cpp b/src/library/coercion.cpp index 90f5c2d235..8b68993b9a 100644 --- a/src/library/coercion.cpp +++ b/src/library/coercion.cpp @@ -146,16 +146,18 @@ static void add_coercion_trans(coercion_ext & ext, io_state const & ios, name co level_param_names const & f_level_params, expr const & f, expr const & f_type, unsigned f_num_args, level_param_names const & g_level_params, expr g, expr const & g_type, unsigned g_num_args) { expr t = f_type; - buffer f_arg_names; - buffer f_arg_types; buffer args; unsigned i = f_num_args; + while (i > 0) { + i--; + args.push_back(mk_var(i)); + } + buffer f_arg_names; + buffer f_arg_types; while (is_pi(t)) { f_arg_names.push_back(binding_name(t)); f_arg_types.push_back(binding_domain(t)); t = binding_body(t); - i--; - args.push_back(mk_var(i)); } expr f_app = apply_beta(f, args.size(), args.data()); expr D_app = t;