diff --git a/src/frontends/lean/register_module.cpp b/src/frontends/lean/register_module.cpp
index e1e410b72..137e5d694 100644
--- a/src/frontends/lean/register_module.cpp
+++ b/src/frontends/lean/register_module.cpp
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 
 namespace lean {
 /** \see parse_lean_expr */
-static int parse_lean_expr_core(lua_State * L, ro_environment const & env, io_state & st) {
+static int parse_lean_expr_core(lua_State * L, ro_shared_environment const & env, io_state & st) {
     char const * src = luaL_checkstring(L, 1);
     std::istringstream in(src);
     script_state S   = to_script_state(L);
@@ -28,7 +28,7 @@ static int parse_lean_expr_core(lua_State * L, ro_environment const & env, io_st
 }
 
 /** \see parse_lean_expr */
-static int parse_lean_expr_core(lua_State * L, ro_environment const & env) {
+static int parse_lean_expr_core(lua_State * L, ro_shared_environment const & env) {
     io_state * io = get_io_state(L);
     if (io == nullptr) {
         io_state s(get_global_options(L), mk_pp_formatter(env));
@@ -59,10 +59,10 @@ static int parse_lean_expr(lua_State * L) {
     */
     int nargs = get_nonnil_top(L);
     if (nargs == 1) {
-        ro_environment env(L); // get global environment
+        ro_shared_environment env(L); // get global environment
         return parse_lean_expr_core(L, env);
     } else {
-        ro_environment env(L, 2);
+        ro_shared_environment env(L, 2);
         if (nargs == 2) {
             return parse_lean_expr_core(L, env);
         } else {
@@ -75,7 +75,7 @@ static int parse_lean_expr(lua_State * L) {
 }
 
 /** \see parse_lean_cmds */
-static void parse_lean_cmds_core(lua_State * L, rw_environment & env, io_state & st) {
+static void parse_lean_cmds_core(lua_State * L, rw_shared_environment & env, io_state & st) {
     char const * src = luaL_checkstring(L, 1);
     std::istringstream in(src);
     script_state S   = to_script_state(L);
@@ -85,7 +85,7 @@ static void parse_lean_cmds_core(lua_State * L, rw_environment & env, io_state &
 }
 
 /** \see parse_lean_cmds */
-static void parse_lean_cmds_core(lua_State * L, rw_environment & env) {
+static void parse_lean_cmds_core(lua_State * L, rw_shared_environment & env) {
     io_state * io = get_io_state(L);
     if (io == nullptr) {
         io_state s(get_global_options(L), mk_pp_formatter(env));
@@ -105,11 +105,11 @@ static int parse_lean_cmds(lua_State * L) {
     */
     int nargs = get_nonnil_top(L);
     if (nargs == 1) {
-        rw_environment env(L); // get global environment
+        rw_shared_environment env(L); // get global environment
         parse_lean_cmds_core(L, env);
         return 0;
     } else {
-        rw_environment env(L, 2);
+        rw_shared_environment env(L, 2);
         if (nargs == 2) {
             parse_lean_cmds_core(L, env);
             return 0;
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index cc0e15d53..b9c920b11 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -621,15 +621,15 @@ environment::extension const * environment::extension::get_parent_core() const {
     return nullptr;
 }
 
-read_only_environment::read_only_environment(environment const & env):
+read_only_shared_environment::read_only_shared_environment(environment const & env):
     m_env(env),
     m_lock(m_env.m_ptr->m_mutex) {
 }
-read_only_environment::~read_only_environment() {}
+read_only_shared_environment::~read_only_shared_environment() {}
 
-read_write_environment::read_write_environment(environment const & env):
+read_write_shared_environment::read_write_shared_environment(environment const & env):
     m_env(env),
     m_lock(m_env.m_ptr->m_mutex) {
 }
-read_write_environment::~read_write_environment() {}
+read_write_shared_environment::~read_write_shared_environment() {}
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index d9ea91013..661cf6531 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -23,8 +23,8 @@ private:
     void check_type(name const & n, expr const & t, expr const & v);
     environment(std::shared_ptr<imp> const & parent, bool);
     explicit environment(std::shared_ptr<imp> const & ptr);
-    friend class read_only_environment;
-    friend class read_write_environment;
+    friend class read_only_shared_environment;
+    friend class read_write_shared_environment;
 public:
     typedef std::weak_ptr<imp> weak_ref;
 
diff --git a/src/kernel/threadsafe_environment.h b/src/kernel/threadsafe_environment.h
index aad2b52c6..f49d2d52d 100644
--- a/src/kernel/threadsafe_environment.h
+++ b/src/kernel/threadsafe_environment.h
@@ -11,31 +11,31 @@ Author: Leonardo de Moura
 namespace lean {
 /**
    \brief The environment object is not thread safe.
-   The helper classes \c read_only_environment and \c read_write_environment
+   The helper classes \c read_only_shared_environment and \c read_write_shared_environment
    provides thread safe access to the environment object.
 
    \remark We do not use these classes internally.
    They are only used for implementing external APIs.
 */
-class read_only_environment {
+class read_only_shared_environment {
     environment   m_env;
     shared_lock   m_lock;
 public:
-    read_only_environment(environment const & env);
-    ~read_only_environment();
+    read_only_shared_environment(environment const & env);
+    ~read_only_shared_environment();
     operator environment const &() const { return m_env; }
     environment const * operator->() const { return &m_env; }
 };
 
 /**
-   \brief See \c read_only_environment
+   \brief See \c read_only_shared_environment
 */
-class read_write_environment {
+class read_write_shared_environment {
     environment     m_env;
     exclusive_lock  m_lock;
 public:
-    read_write_environment(environment const & env);
-    ~read_write_environment();
+    read_write_shared_environment(environment const & env);
+    ~read_write_shared_environment();
     operator environment &() { return m_env; }
     environment * operator->() { return &m_env; }
 };
diff --git a/src/library/hidden_defs.cpp b/src/library/hidden_defs.cpp
index 127b43193..f90182568 100644
--- a/src/library/hidden_defs.cpp
+++ b/src/library/hidden_defs.cpp
@@ -68,14 +68,14 @@ void hide_builtin(environment & env) {
 }
 
 static int is_hidden(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     lua_pushboolean(L, is_hidden(env, to_name_ext(L, 2)));
     return 1;
 }
 
 static int set_hidden_flag(lua_State * L) {
     int nargs = lua_gettop(L);
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     set_hidden_flag(env, to_name_ext(L, 2), nargs <= 2 ? true : lua_toboolean(L, 3));
     return 0;
 }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index ff9851e95..3b176456e 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -833,7 +833,7 @@ static int formatter_call_core(lua_State * L) {
         } else if (is_context(L, 2)) {
             return push_format(L, fmt(to_context(L, 2), opts));
         } else if (is_environment(L, 2)) {
-            ro_environment env(L, 2);
+            ro_shared_environment env(L, 2);
             return push_format(L, fmt(env, opts));
         } else if (is_object(L, 2)) {
             return push_format(L, fmt(to_object(L, 2), opts));
@@ -853,7 +853,7 @@ static int formatter_call(lua_State * L) {
     formatter & fmt = to_formatter(L, 1);
     optional<environment> env = fmt.get_environment();
     if (env) {
-        read_only_environment ro_env(*env);
+        read_only_shared_environment ro_env(*env);
         return formatter_call_core(L);
     } else {
         return formatter_call_core(L);
@@ -930,20 +930,20 @@ DECL_UDATA(environment)
 
 static environment get_global_environment(lua_State * L);
 
-ro_environment::ro_environment(lua_State * L, int idx):
-    read_only_environment(to_environment(L, idx)) {
+ro_shared_environment::ro_shared_environment(lua_State * L, int idx):
+    read_only_shared_environment(to_environment(L, idx)) {
 }
 
-ro_environment::ro_environment(lua_State * L):
-    read_only_environment(get_global_environment(L)) {
+ro_shared_environment::ro_shared_environment(lua_State * L):
+    read_only_shared_environment(get_global_environment(L)) {
 }
 
-rw_environment::rw_environment(lua_State * L, int idx):
-    read_write_environment(to_environment(L, idx)) {
+rw_shared_environment::rw_shared_environment(lua_State * L, int idx):
+    read_write_shared_environment(to_environment(L, idx)) {
 }
 
-rw_environment::rw_environment(lua_State * L):
-    read_write_environment(get_global_environment(L)) {
+rw_shared_environment::rw_shared_environment(lua_State * L):
+    read_write_shared_environment(get_global_environment(L)) {
 }
 
 static int mk_empty_environment(lua_State * L) {
@@ -951,31 +951,31 @@ static int mk_empty_environment(lua_State * L) {
 }
 
 static int environment_mk_child(lua_State * L) {
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     return push_environment(L, env->mk_child());
 }
 
 static int environment_has_parent(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     lua_pushboolean(L, env->has_parent());
     return 1;
 }
 
 static int environment_has_children(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     lua_pushboolean(L, env->has_children());
     return 1;
 }
 
 static int environment_parent(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     if (!env->has_parent())
         throw exception("environment does not have a parent environment");
     return push_environment(L, env->parent());
 }
 
 static int environment_add_uvar(lua_State * L) {
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
         env->add_uvar(to_name_ext(L, 2));
@@ -985,18 +985,18 @@ static int environment_add_uvar(lua_State * L) {
 }
 
 static int environment_is_ge(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     lua_pushboolean(L, env->is_ge(to_level(L, 2), to_level(L, 3)));
     return 1;
 }
 
 static int environment_get_uvar(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     return push_level(L, env->get_uvar(to_name_ext(L, 2)));
 }
 
 static int environment_add_definition(lua_State * L) {
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 3) {
         env->add_definition(to_name_ext(L, 2), to_expr(L, 3));
@@ -1012,36 +1012,36 @@ static int environment_add_definition(lua_State * L) {
 }
 
 static int environment_add_theorem(lua_State * L) {
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     env->add_theorem(to_name_ext(L, 2), to_expr(L, 3), to_expr(L, 4));
     return 0;
 }
 
 static int environment_add_var(lua_State * L) {
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     env->add_var(to_name_ext(L, 2), to_expr(L, 3));
     return 0;
 }
 
 static int environment_add_axiom(lua_State * L) {
-    rw_environment env(L, 1);
+    rw_shared_environment env(L, 1);
     env->add_axiom(to_name_ext(L, 2), to_expr(L, 3));
     return 0;
 }
 
 static int environment_find_object(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     return push_optional_object(L, env->find_object(to_name_ext(L, 2)));
 }
 
 static int environment_has_object(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     lua_pushboolean(L, env->has_object(to_name_ext(L, 2)));
     return 1;
 }
 
 static int environment_check_type(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
         return push_expr(L, env->infer_type(to_expr(L, 2)));
@@ -1050,7 +1050,7 @@ static int environment_check_type(lua_State * L) {
 }
 
 static int environment_normalize(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     int nargs = lua_gettop(L);
     if (nargs == 2)
         return push_expr(L, env->normalize(to_expr(L, 2)));
@@ -1065,7 +1065,7 @@ static int environment_normalize(lua_State * L) {
    \see environment_local_objects.
 */
 static int environment_next_object(lua_State * L) {
-    ro_environment env(L, lua_upvalueindex(1));
+    ro_shared_environment env(L, lua_upvalueindex(1));
     unsigned i   = lua_tointeger(L, lua_upvalueindex(2));
     unsigned num = lua_tointeger(L, lua_upvalueindex(3));
     if (i >= num) {
@@ -1080,7 +1080,7 @@ static int environment_next_object(lua_State * L) {
 }
 
 static int environment_objects_core(lua_State * L, bool local) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     push_environment(L, env);   // upvalue(1): environment
     lua_pushinteger(L, 0);      // upvalue(2): index
     lua_pushinteger(L, env->get_num_objects(local)); // upvalue(3): size
@@ -1107,7 +1107,7 @@ static int environment_infer_type(lua_State * L) {
 }
 
 static int environment_tostring(lua_State * L) {
-    ro_environment env(L, 1);
+    ro_shared_environment env(L, 1);
     std::ostringstream out;
     formatter fmt = get_global_formatter(L);
     options opts  = get_global_options(L);
diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h
index 04c944bdf..6476980f4 100644
--- a/src/library/kernel_bindings.h
+++ b/src/library/kernel_bindings.h
@@ -57,19 +57,19 @@ public:
    \brief Helper class for getting a read-only reference
    for an environment object on the Lua stack.
 */
-class ro_environment : public read_only_environment {
+class ro_shared_environment : public read_only_shared_environment {
 public:
-    ro_environment(lua_State * L, int idx);
-    ro_environment(lua_State * L);
+    ro_shared_environment(lua_State * L, int idx);
+    ro_shared_environment(lua_State * L);
 };
 
 /**
    \brief Helper class for getting a read-write reference
    for an environment object on the Lua stack.
 */
-class rw_environment : public read_write_environment {
+class rw_shared_environment : public read_write_shared_environment {
 public:
-    rw_environment(lua_State * L, int idx);
-    rw_environment(lua_State * L);
+    rw_shared_environment(lua_State * L, int idx);
+    rw_shared_environment(lua_State * L);
 };
 }
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index b3783f932..1777efeea 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -559,7 +559,7 @@ static int tactic_call_core(lua_State * L, tactic t, environment env, io_state i
 static int tactic_call(lua_State * L) {
     int nargs = lua_gettop(L);
     tactic t = to_tactic_ext(L, 1);
-    ro_environment env(L, 2);
+    ro_shared_environment env(L, 2);
     if (nargs == 3) {
         io_state * ios = get_io_state(L);
         check_ios(ios);
@@ -646,7 +646,7 @@ static int tactic_solve_core(lua_State * L, tactic t, environment env, io_state
 static int tactic_solve(lua_State * L) {
     int nargs = lua_gettop(L);
     tactic t = to_tactic_ext(L, 1);
-    ro_environment env(L, 2);
+    ro_shared_environment env(L, 2);
     if (nargs == 3) {
         io_state * ios = get_io_state(L);
         check_ios(ios);