From 73acaca21e2b9789509e29b131d50e2b003fc565 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 7 Feb 2015 19:05:46 -0800
Subject: [PATCH] refactor(kernel/default_converter): remove extra_opaque_pred

---
 src/kernel/default_converter.cpp | 9 ++-------
 src/kernel/default_converter.h   | 3 ---
 2 files changed, 2 insertions(+), 10 deletions(-)

diff --git a/src/kernel/default_converter.cpp b/src/kernel/default_converter.cpp
index c599627a6..b3b8efd1f 100644
--- a/src/kernel/default_converter.cpp
+++ b/src/kernel/default_converter.cpp
@@ -14,16 +14,12 @@ Author: Leonardo de Moura
 namespace lean {
 static expr * g_dont_care = nullptr;
 
-default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
-                                     extra_opaque_pred const & pred):
-    m_env(env), m_module_idx(mod_idx), m_memoize(memoize), m_extra_pred(pred) {
+default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
+    m_env(env), m_module_idx(mod_idx), m_memoize(memoize) {
     m_tc  = nullptr;
     m_jst = nullptr;
 }
 
-default_converter::default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize):
-    default_converter(env, mod_idx, memoize, [](name const &) { return false; }) {}
-
 default_converter::default_converter(environment const & env, bool relax_main_opaque, bool memoize):
     default_converter(env, relax_main_opaque ? optional<module_idx>(0) : optional<module_idx>(), memoize) {}
 
@@ -114,7 +110,6 @@ expr default_converter::whnf_core(expr const & e) {
 bool default_converter::is_opaque(declaration const & d) const {
     lean_assert(d.is_definition());
     if (d.is_theorem()) return true;                               // theorems are always opaque
-    if (m_extra_pred(d.get_name())) return true;                   // extra_opaque predicate overrides opaque flag
     if (!d.is_opaque()) return false;                              // d is a transparent definition
     if (m_module_idx && d.get_module_idx() == *m_module_idx) return false; // the opaque definitions in mod_idx are considered transparent
     return true;                                                   // d is opaque
diff --git a/src/kernel/default_converter.h b/src/kernel/default_converter.h
index c6f35056d..5dfb334e0 100644
--- a/src/kernel/default_converter.h
+++ b/src/kernel/default_converter.h
@@ -18,7 +18,6 @@ protected:
     environment                                 m_env;
     optional<module_idx>                        m_module_idx;
     bool                                        m_memoize;
-    extra_opaque_pred                           m_extra_pred;
     expr_struct_map<expr>                       m_whnf_core_cache;
     expr_struct_map<pair<expr, constraint_seq>> m_whnf_cache;
 
@@ -72,8 +71,6 @@ protected:
     pair<bool, constraint_seq> is_def_eq(expr const & t, expr const & s);
 
 public:
-    default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize,
-                      extra_opaque_pred const & pred);
     default_converter(environment const & env, optional<module_idx> mod_idx, bool memoize = true);
     default_converter(environment const & env, bool relax_main_opaque, bool memoize = true);