From 256112be5b7188821cdee059244cc79bf6171bdd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Oct 2018 15:25:57 -0700
Subject: [PATCH] chore(library/compiler/lcnf): disable lambda eta-expansion
 during LCNF conversion

We should do it at `csimp`
---
 src/library/compiler/lcnf.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 8694d83ab7..b399569866 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -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);