diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index f9441941e4..e7051de89d 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,6 +1,7 @@
 add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   kernel_bindings.cpp io_state_stream.cpp bin_app.cpp
-  resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp normalize.cpp)
+  resolve_macro.cpp kernel_serializer.cpp max_sharing.cpp
+  normalize.cpp shared_environment.cpp)
 # placeholder.cpp fo_unify.cpp hop_match.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})
diff --git a/src/library/shared_environment.cpp b/src/library/shared_environment.cpp
new file mode 100644
index 0000000000..a0263a6134
--- /dev/null
+++ b/src/library/shared_environment.cpp
@@ -0,0 +1,32 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/shared_environment.h"
+
+namespace lean {
+shared_environment::shared_environment() {}
+shared_environment::shared_environment(environment const & env):m_env(env) {}
+
+environment shared_environment::get_environment() const {
+    shared_lock l(m_mutex);
+    return m_env;
+}
+
+void shared_environment::add(certified_declaration const & d) {
+    exclusive_lock l(m_mutex);
+    m_env = m_env.add(d);
+}
+
+void shared_environment::replace(certified_declaration const & t) {
+    exclusive_lock l(m_mutex);
+    m_env = m_env.replace(t);
+}
+
+void shared_environment::update(std::function<environment(environment const &)> const & f) {
+    exclusive_lock l(m_mutex);
+    m_env = f(m_env);
+}
+}
diff --git a/src/library/shared_environment.h b/src/library/shared_environment.h
new file mode 100644
index 0000000000..70998f08c8
--- /dev/null
+++ b/src/library/shared_environment.h
@@ -0,0 +1,40 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <functional>
+#include "util/shared_mutex.h"
+#include "kernel/environment.h"
+
+namespace lean {
+/** \brief Auxiliary object used when multiple threads are trying to populate the same environment. */
+class shared_environment {
+    environment          m_env;
+    mutable shared_mutex m_mutex;
+public:
+    shared_environment();
+    shared_environment(environment const & env);
+    /** \brief Return a copy of the current environment. This is a constant time operation. */
+    environment get_environment() const;
+    /**
+        \brief Add the given certified declaration to the environment.
+        This is a constant time operation.
+        It blocks this object for a small amount of time.
+    */
+    void add(certified_declaration const & d);
+    /**
+        \brief Replace the axiom with name <tt>t.get_declaration().get_name()</tt> with the theorem t.get_declaration().
+        This is a constant time operation.
+        It blocks this object for a small amount of time.
+    */
+    void replace(certified_declaration const & t);
+    /**
+       \brief Update the environment using the given function.
+       This procedure blocks access to this object.
+    */
+    void update(std::function<environment(environment const &)> const & f);
+};
+}