From af039f420afb255ca55a48085d103cdccd942dc6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 6 Mar 2019 05:26:53 -0800 Subject: [PATCH] chore(util): remove dead code --- src/util/CMakeLists.txt | 3 +-- src/util/name_map.cpp | 17 ----------------- src/util/name_map.h | 8 -------- 3 files changed, 1 insertion(+), 27 deletions(-) delete mode 100644 src/util/name_map.cpp diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 6a9388fe40..ba97c34e94 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -1,6 +1,5 @@ add_library(util OBJECT object_ref.cpp name.cpp name_set.cpp fresh_name.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp ascii.cpp shared_mutex.cpp path.cpp lean_path.cpp lbool.cpp bitap_fuzzy_search.cpp - init_module.cpp name_map.cpp list_fn.cpp file_lock.cpp - timeit.cpp timer.cpp cancellable.cpp + init_module.cpp list_fn.cpp file_lock.cpp timeit.cpp timer.cpp cancellable.cpp parser_exception.cpp name_generator.cpp kvmap.cpp) diff --git a/src/util/name_map.cpp b/src/util/name_map.cpp deleted file mode 100644 index 2f56b194a1..0000000000 --- a/src/util/name_map.cpp +++ /dev/null @@ -1,17 +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 "util/name_map.h" - -namespace lean { -name const & rename_map::find(name const & k) const { - name const * it = &k; - while (name const * new_it = name_map::find(*it)) { - it = new_it; - } - return *it; -} -} diff --git a/src/util/name_map.h b/src/util/name_map.h index 0562ada612..d0f95667d9 100644 --- a/src/util/name_map.h +++ b/src/util/name_map.h @@ -9,12 +9,4 @@ Author: Leonardo de Moura #include "util/name.h" namespace lean { template using name_map = rb_map; - -class rename_map : public name_map { -public: - // Similar to name_map::find, but it "follows" the sequence of renames. - // Example, if map contains "A->B" and "B->C", then find(A) returns C. - // Moreover, if k is not in the map, the result is \c k - name const & find(name const & k) const; -}; }