From 9e08cab381ea28c062ed7763fddb7b4f2049de19 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Feb 2018 10:30:52 -0800
Subject: [PATCH] chore(library/type_context): simplify cache management

---
 src/library/type_context.cpp | 16 +---------------
 src/library/type_context.h   |  2 --
 2 files changed, 1 insertion(+), 17 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 197d3a6ef3..64f08bf069 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -183,19 +183,7 @@ type_context_cache_ptr type_context_cache_manager::mk(environment const & env, o
         m_cache_ptr->m_options = o;
         return release();
     }
-    if (!env.is_descendant(m_env) ||
-        get_reducibility_fingerprint(env) != m_reducibility_fingerprint ||
-        get_instance_fingerprint(env) != m_instance_fingerprint) {
-        lean_trace("type_context_cache",
-                   bool c1 = (get_reducibility_fingerprint(env) == m_reducibility_fingerprint);
-                   bool c2 = (get_instance_fingerprint(env) == m_instance_fingerprint);
-                   tout() << "creating new cache, is_descendant: " << env.is_descendant(m_env)
-                   << ", reducibility compatibility: " << c1 << ", instance compatibility: " << c2 << "\n";);
-        return mk_cache(env, o, m_use_bi);
-    }
-    m_cache_ptr->m_options = o;
-    m_cache_ptr->m_env     = env;
-    return release();
+    return mk_cache(env, o, m_use_bi);
 }
 
 void type_context_cache_manager::recycle(type_context_cache_ptr const & ptr) {
@@ -203,8 +191,6 @@ void type_context_cache_manager::recycle(type_context_cache_ptr const & ptr) {
     m_cache_ptr = ptr;
     if (!is_eqp(ptr->m_env, m_env)) {
         m_env = ptr->m_env;
-        m_reducibility_fingerprint = get_reducibility_fingerprint(ptr->m_env);
-        m_instance_fingerprint     = get_instance_fingerprint(ptr->m_env);
     }
     if (!ptr->m_instance_fingerprint) {
         ptr->m_instance_cache.clear();
diff --git a/src/library/type_context.h b/src/library/type_context.h
index f8a18b0841..9262e486e3 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -164,8 +164,6 @@ typedef std::shared_ptr<type_context_cache> type_context_cache_ptr;
    to try to reuse type_context_cache objects */
 class type_context_cache_manager {
     type_context_cache_ptr m_cache_ptr;
-    unsigned               m_reducibility_fingerprint;
-    unsigned               m_instance_fingerprint;
     environment            m_env;
     unsigned               m_max_depth;
     bool                   m_use_bi;