diff --git a/src/library/shared_environment.cpp b/src/library/shared_environment.cpp index f165bafa4..b60b76e10 100644 --- a/src/library/shared_environment.cpp +++ b/src/library/shared_environment.cpp @@ -11,27 +11,27 @@ 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); + unique_lock l(m_mutex); return m_env; } void shared_environment::add(certified_declaration const & d) { - exclusive_lock l(m_mutex); + unique_lock l(m_mutex); m_env = m_env.add(d); } void shared_environment::add(declaration const & d) { - exclusive_lock l(m_mutex); + unique_lock l(m_mutex); m_env = m_env.add(d); } void shared_environment::replace(certified_declaration const & t) { - exclusive_lock l(m_mutex); + unique_lock l(m_mutex); m_env = m_env.replace(t); } void shared_environment::update(std::function const & f) { - exclusive_lock l(m_mutex); + unique_lock l(m_mutex); m_env = f(m_env); } } diff --git a/src/library/shared_environment.h b/src/library/shared_environment.h index 3a52a2a03..eb68e06ff 100644 --- a/src/library/shared_environment.h +++ b/src/library/shared_environment.h @@ -13,7 +13,7 @@ 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; + mutable mutex m_mutex; public: shared_environment(); shared_environment(environment const & env);