diff --git a/src/bindings/lua/options.cpp b/src/bindings/lua/options.cpp
index e4d717f7f9..a1d6d02f00 100644
--- a/src/bindings/lua/options.cpp
+++ b/src/bindings/lua/options.cpp
@@ -25,7 +25,7 @@ options & to_options(lua_State * L, int idx) {
     return *static_cast<options*>(luaL_checkudata(L, idx, options_mt));
 }
 
-static int push_options(lua_State * L, options const & o) {
+int push_options(lua_State * L, options const & o) {
     void * mem = lua_newuserdata(L, sizeof(options));
     new (mem) options(o);
     luaL_getmetatable(L, options_mt);
diff --git a/src/bindings/lua/options.h b/src/bindings/lua/options.h
index c55eff8f26..81333a6a62 100644
--- a/src/bindings/lua/options.h
+++ b/src/bindings/lua/options.h
@@ -11,5 +11,6 @@ class options;
 void open_options(lua_State * L);
 bool is_options(lua_State * L, int idx);
 options & to_options(lua_State * L, int idx);
+int push_options(lua_State * L, options const & o);
 }
 #endif
diff --git a/src/bindings/lua/sexpr.cpp b/src/bindings/lua/sexpr.cpp
index 6d1579e21b..ddb42764a8 100644
--- a/src/bindings/lua/sexpr.cpp
+++ b/src/bindings/lua/sexpr.cpp
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 namespace lean {
 constexpr char const * sexpr_mt = "sexpr.mt";
 
-static int push_sexpr(lua_State * L, sexpr const & e) {
+int push_sexpr(lua_State * L, sexpr const & e) {
     void * mem = lua_newuserdata(L, sizeof(sexpr));
     new (mem) sexpr(e);
     luaL_getmetatable(L, sexpr_mt);
diff --git a/src/bindings/lua/sexpr.h b/src/bindings/lua/sexpr.h
index 431c166126..40c11efacc 100644
--- a/src/bindings/lua/sexpr.h
+++ b/src/bindings/lua/sexpr.h
@@ -11,5 +11,6 @@ class sexpr;
 void open_sexpr(lua_State * L);
 bool is_sexpr(lua_State * L, int idx);
 sexpr & to_sexpr(lua_State * L, int idx);
+int push_sexpr(lua_State * L, sexpr const & e);
 }
 #endif