From 5e9f2e4e6abaf34e3efc16ed97754a8e12c9d87f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 17 Apr 2019 07:14:35 -0700 Subject: [PATCH] chore(library/compiler/specialize): remove leftover that is now a noop --- src/library/compiler/specialize.cpp | 9 --------- 1 file changed, 9 deletions(-) diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index 670cbe102c..fca49a405a 100644 --- a/src/library/compiler/specialize.cpp +++ b/src/library/compiler/specialize.cpp @@ -936,14 +936,6 @@ class specialize_fn { name n = pre_decl.fst(); expr code = pre_decl.snd(); flet save_lctx(m_lctx, m_lctx); - buffer new_fvars; - while (is_lambda(code)) { - expr type = instantiate_rev(binding_domain(code), new_fvars.size(), new_fvars.data()); - expr new_fvar = m_lctx.mk_local_decl(ngen(), binding_name(code), type, binding_info(code)); - new_fvars.push_back(new_fvar); - code = binding_body(code); - } - code = instantiate_rev(code, new_fvars.size(), new_fvars.data()); /* Add fvars decls */ type_checker tc(m_st, m_lctx); buffer new_let_decls; @@ -953,7 +945,6 @@ class specialize_fn { expr new_fvar = m_lctx.mk_local_decl(fvar_name(fvars[i]), y.append_after(i+1), type, fvar_vals[i]).mk_ref(); new_let_decls.push_back(new_fvar); } - code = m_lctx.mk_lambda(new_fvars, code); code = m_lctx.mk_lambda(new_let_decls, code); // lean_trace(name("compiler", "spec_info"), tout() << "STEP 1 " << n << "\n" << code << "\n";); code = abstract_spec_ctx(ctx, code);