chore(library/compiler/lcnf): disable lambda eta-expansion during LCNF conversion

We should do it at `csimp`
This commit is contained in:
Leonardo de Moura 2018-10-09 15:25:57 -07:00
parent 27e6f7f424
commit 256112be5b

View file

@ -436,7 +436,6 @@ public:
expr visit_lambda(expr e, bool root) {
lean_assert(is_lambda(e));
e = type_checker(m_st, m_lctx).eta_expand(e);
expr r;
{
flet<local_ctx> save_lctx(m_lctx, m_lctx);