diff --git a/src/bindings/lua/CMakeLists.txt b/src/bindings/lua/CMakeLists.txt
index 200273892..0dd46d967 100644
--- a/src/bindings/lua/CMakeLists.txt
+++ b/src/bindings/lua/CMakeLists.txt
@@ -1,5 +1,5 @@
 add_library(lua util.cpp lua_exception.cpp name.cpp numerics.cpp
-lua_ref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp
+lref.cpp splay_map.cpp options.cpp sexpr.cpp format.cpp level.cpp
 local_context.cpp expr.cpp context.cpp object.cpp environment.cpp
 formatter.cpp state.cpp leanlua_state.cpp)
 
diff --git a/src/bindings/lua/lua_ref.cpp b/src/bindings/lua/lref.cpp
similarity index 81%
rename from src/bindings/lua/lua_ref.cpp
rename to src/bindings/lua/lref.cpp
index 112d8eb8e..635e26f01 100644
--- a/src/bindings/lua/lua_ref.cpp
+++ b/src/bindings/lua/lref.cpp
@@ -6,17 +6,17 @@ Author: Leonardo de Moura
 */
 #include "util/debug.h"
 #include "bindings/lua/util.h"
-#include "bindings/lua/lua_ref.h"
+#include "bindings/lua/lref.h"
 
 namespace lean {
-lua_ref::lua_ref(lua_State * L, int i) {
+lref::lref(lua_State * L, int i) {
     lean_assert(L);
     m_state = L;
     lua_pushvalue(m_state, i);
     m_ref   = luaL_ref(m_state, LUA_REGISTRYINDEX);
 }
 
-lua_ref::lua_ref(lua_ref const & r) {
+lref::lref(lref const & r) {
     m_state = r.m_state;
     if (m_state) {
         r.push();
@@ -24,18 +24,18 @@ lua_ref::lua_ref(lua_ref const & r) {
     }
 }
 
-lua_ref::lua_ref(lua_ref && r) {
+lref::lref(lref && r) {
     m_state = r.m_state;
     m_ref   = r.m_ref;
     r.m_state = nullptr;
 }
 
-lua_ref::~lua_ref() {
+lref::~lref() {
     if (m_state)
         luaL_unref(m_state, LUA_REGISTRYINDEX, m_ref);
 }
 
-lua_ref & lua_ref::operator=(lua_ref const & r) {
+lref & lref::operator=(lref const & r) {
     if (m_ref == r.m_ref)
         return *this;
     if (m_state)
@@ -48,12 +48,12 @@ lua_ref & lua_ref::operator=(lua_ref const & r) {
     return *this;
 }
 
-void lua_ref::push() const {
+void lref::push() const {
     lean_assert(m_state);
     lua_rawgeti(m_state, LUA_REGISTRYINDEX, m_ref);
 }
 
-int lua_ref_lt_proc::operator()(lua_ref const & r1, lua_ref const & r2) const {
+int lref_lt_proc::operator()(lref const & r1, lref const & r2) const {
     lean_assert(r1.get_state() == r2.get_state());
     lua_State * L = r1.get_state();
     r1.push();
diff --git a/src/bindings/lua/lua_ref.h b/src/bindings/lua/lref.h
similarity index 59%
rename from src/bindings/lua/lua_ref.h
rename to src/bindings/lua/lref.h
index 7f65817b4..b3213cedd 100644
--- a/src/bindings/lua/lua_ref.h
+++ b/src/bindings/lua/lref.h
@@ -10,27 +10,27 @@ namespace lean {
 /**
    \brief Reference to Lua object.
 */
-class lua_ref {
+class lref {
     lua_State * m_state;
     int         m_ref;
 public:
-    lua_ref():m_state(nullptr) {}
+    lref():m_state(nullptr) {}
     /**
        \brief Create a reference to the Lua object at position \c i on \c L stack.
     */
-    lua_ref(lua_State * L, int i);
-    lua_ref(lua_ref const & r);
-    lua_ref(lua_ref && r);
-    ~lua_ref();
-    lua_ref & operator=(lua_ref const & r);
+    lref(lua_State * L, int i);
+    lref(lref const & r);
+    lref(lref && r);
+    ~lref();
+    lref & operator=(lref const & r);
     void push() const;
     lua_State * get_state() const { return m_state; }
 };
 
 /**
-   \brief '<' functor for lua_ref.
+   \brief '<' functor for lref.
 */
-struct lua_ref_lt_proc {
-    int operator()(lua_ref const & r1, lua_ref const & r2) const;
+struct lref_lt_proc {
+    int operator()(lref const & r1, lref const & r2) const;
 };
 }
diff --git a/src/bindings/lua/splay_map.cpp b/src/bindings/lua/splay_map.cpp
index 5c20bc6c8..2260e1a1b 100644
--- a/src/bindings/lua/splay_map.cpp
+++ b/src/bindings/lua/splay_map.cpp
@@ -7,10 +7,10 @@ Author: Leonardo de Moura
 #include <lua.hpp>
 #include "util/splay_map.h"
 #include "bindings/lua/util.h"
-#include "bindings/lua/lua_ref.h"
+#include "bindings/lua/lref.h"
 
 namespace lean {
-typedef splay_map<lua_ref, lua_ref, lua_ref_lt_proc> lua_splay_map;
+typedef splay_map<lref, lref, lref_lt_proc> lua_splay_map;
 
 constexpr char const * splay_map_mt = "splay_map.mt";
 
@@ -46,7 +46,7 @@ static int splay_map_size(lua_State * L) {
 }
 
 static int splay_map_contains(lua_State * L) {
-    lua_pushboolean(L, to_splay_map(L, 1).contains(lua_ref(L, 2)));
+    lua_pushboolean(L, to_splay_map(L, 1).contains(lref(L, 2)));
     return 1;
 }
 
@@ -56,18 +56,18 @@ static int splay_map_empty(lua_State * L) {
 }
 
 static int splay_map_insert(lua_State * L) {
-    to_splay_map(L, 1).insert(lua_ref(L, 2), lua_ref(L, 3));
+    to_splay_map(L, 1).insert(lref(L, 2), lref(L, 3));
     return 0;
 }
 
 static int splay_map_erase(lua_State * L) {
-    to_splay_map(L, 1).erase(lua_ref(L, 2));
+    to_splay_map(L, 1).erase(lref(L, 2));
     return 0;
 }
 
 static int splay_map_find(lua_State * L) {
     lua_splay_map & m = to_splay_map(L, 1);
-    lua_ref * val = m.splay_find(lua_ref(L, 2));
+    lref * val = m.splay_find(lref(L, 2));
     if (val) {
         lean_assert(val->get_state() == L);
         val->push();
@@ -93,7 +93,7 @@ static int splay_map_for_each(lua_State * L) {
     // The copy operation is very cheap O(1).
     lua_splay_map m(to_splay_map(L, 1)); // map
     luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
-    m.for_each([&](lua_ref const & k, lua_ref const & v) {
+    m.for_each([&](lref const & k, lref const & v) {
         lua_pushvalue(L, 2); // push user-fun
         k.push();
         v.push();