From 3e4594d6be9821df0495203bf05cbf66eaaa6cf8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 12 Apr 2018 11:06:36 -0700
Subject: [PATCH] chore(library/shared_environment): remove dead file

---
 src/library/CMakeLists.txt         |  3 +--
 src/library/shared_environment.cpp | 32 -----------------------
 src/library/shared_environment.h   | 41 ------------------------------
 3 files changed, 1 insertion(+), 75 deletions(-)
 delete mode 100644 src/library/shared_environment.cpp
 delete mode 100644 src/library/shared_environment.h

diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 566be6e65f..7ccbec1af6 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,7 +1,6 @@
 add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   io_state_stream.cpp bin_app.cpp constants.cpp kernel_serializer.cpp
-  max_sharing.cpp shared_environment.cpp module.cpp
-  private.cpp placeholder.cpp aliases.cpp
+  max_sharing.cpp module.cpp private.cpp placeholder.cpp aliases.cpp
   update_declaration.cpp scoped_ext.cpp sorry.cpp replace_visitor.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp
   class.cpp util.cpp print.cpp annotation.cpp quote.cpp
diff --git a/src/library/shared_environment.cpp b/src/library/shared_environment.cpp
deleted file mode 100644
index 51740deb81..0000000000
--- a/src/library/shared_environment.cpp
+++ /dev/null
@@ -1,32 +0,0 @@
-/*
-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 {
-    lock_guard<mutex> l(m_mutex);
-    return m_env;
-}
-
-void shared_environment::add(certified_declaration const & d) {
-    lock_guard<mutex> l(m_mutex);
-    m_env = m_env.add(d);
-}
-
-void shared_environment::replace(certified_declaration const & t) {
-    lock_guard<mutex> l(m_mutex);
-    m_env = m_env.replace(t);
-}
-
-void shared_environment::update(std::function<environment(environment const &)> const & f) {
-    lock_guard<mutex> l(m_mutex);
-    m_env = f(m_env);
-}
-}
diff --git a/src/library/shared_environment.h b/src/library/shared_environment.h
deleted file mode 100644
index 4870745208..0000000000
--- a/src/library/shared_environment.h
+++ /dev/null
@@ -1,41 +0,0 @@
-/*
-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 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;
-    environment env() const { return get_environment(); }
-    /**
-        \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);
-};
-}