diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0295e53d4..ed99fb269 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -161,7 +161,7 @@ add_subdirectory(library/tactic)
 set(LEAN_LIBS ${LEAN_LIBS} tactic)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
-add_subdirectory(bindings/lua)
+add_subdirectory(frontends/lua)
 set(LEAN_LIBS ${LEAN_LIBS} leanlua)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
diff --git a/src/bindings/lua/CMakeLists.txt b/src/frontends/lua/CMakeLists.txt
similarity index 100%
rename from src/bindings/lua/CMakeLists.txt
rename to src/frontends/lua/CMakeLists.txt
diff --git a/src/bindings/lua/frontend_lean.cpp b/src/frontends/lua/frontend_lean.cpp
similarity index 99%
rename from src/bindings/lua/frontend_lean.cpp
rename to src/frontends/lua/frontend_lean.cpp
index 04c452fee..270d4239e 100644
--- a/src/bindings/lua/frontend_lean.cpp
+++ b/src/frontends/lua/frontend_lean.cpp
@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "library/io_state.h"
 #include "library/kernel_bindings.h"
 #include "frontends/lean/parser.h"
-#include "bindings/lua/leanlua_state.h"
+#include "frontends/lua/leanlua_state.h"
 
 namespace lean {
 /** \see parse_lean_expr */
diff --git a/src/bindings/lua/frontend_lean.h b/src/frontends/lua/frontend_lean.h
similarity index 100%
rename from src/bindings/lua/frontend_lean.h
rename to src/frontends/lua/frontend_lean.h
diff --git a/src/bindings/lua/lean.lua b/src/frontends/lua/lean.lua
similarity index 100%
rename from src/bindings/lua/lean.lua
rename to src/frontends/lua/lean.lua
diff --git a/src/bindings/lua/leanlua_state.cpp b/src/frontends/lua/leanlua_state.cpp
similarity index 99%
rename from src/bindings/lua/leanlua_state.cpp
rename to src/frontends/lua/leanlua_state.cpp
index f004210cc..4332cd474 100644
--- a/src/bindings/lua/leanlua_state.cpp
+++ b/src/frontends/lua/leanlua_state.cpp
@@ -24,9 +24,9 @@ Author: Leonardo de Moura
 #include "library/tactic/open_module.h"
 #include "library/elaborator/elaborator_exception.h"
 #include "frontends/lean/frontend.h"
-#include "bindings/lua/leanlua_state.h"
-#include "bindings/lua/frontend_lean.h"
-#include "bindings/lua/lean.lua"
+#include "frontends/lua/leanlua_state.h"
+#include "frontends/lua/frontend_lean.h"
+#include "frontends/lua/lean.lua"
 
 extern "C" void * lua_realloc(void *, void * q, size_t, size_t new_size) { return lean::realloc(q, new_size); }
 
@@ -71,6 +71,7 @@ struct leanlua_state::imp {
         open_kernel_module(m_state);
         open_arith_module(m_state);
         open_tactic_module(m_state);
+        open_frontend_lean(m_state);
         open_extra(m_state);
 
         dostring(g_leanlua_extra);
diff --git a/src/bindings/lua/leanlua_state.h b/src/frontends/lua/leanlua_state.h
similarity index 100%
rename from src/bindings/lua/leanlua_state.h
rename to src/frontends/lua/leanlua_state.h
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 078154dbc..afb40579d 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"
-#include "bindings/lua/leanlua_state.h"
+#include "frontends/lua/leanlua_state.h"
 #include "version.h"
 
 using lean::shell;