From d2cbd2598567ea5d968ea10c88a2db5c38c01133 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 17 Oct 2014 10:23:35 -0700
Subject: [PATCH] refactor(kernel): replace_visitor doesn't need to be in the
 kernel anymore

---
 src/kernel/CMakeLists.txt                   | 2 +-
 src/library/CMakeLists.txt                  | 2 +-
 src/{kernel => library}/replace_visitor.cpp | 2 +-
 src/{kernel => library}/replace_visitor.h   | 0
 src/library/tactic/tactic.cpp               | 2 +-
 5 files changed, 4 insertions(+), 4 deletions(-)
 rename src/{kernel => library}/replace_visitor.cpp (98%)
 rename src/{kernel => library}/replace_visitor.h (100%)

diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 01e5ffa1b..334a0ee87 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,6 +1,6 @@
 add_library(kernel level.cpp expr.cpp expr_eq_fn.cpp for_each_fn.cpp
 replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
-formatter.cpp declaration.cpp replace_visitor.cpp environment.cpp
+formatter.cpp declaration.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
 normalizer_extension.cpp init_module.cpp)
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index e1bbbe7c7..7c499fe67 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -4,7 +4,7 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   normalize.cpp shared_environment.cpp module.cpp coercion.cpp
   private.cpp placeholder.cpp aliases.cpp level_names.cpp
   update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
-  standard_kernel.cpp sorry.cpp
+  standard_kernel.cpp sorry.cpp replace_visitor.cpp
   unifier.cpp unifier_plugin.cpp inductive_unifier_plugin.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp match.cpp
   definition_cache.cpp declaration_index.cpp
diff --git a/src/kernel/replace_visitor.cpp b/src/library/replace_visitor.cpp
similarity index 98%
rename from src/kernel/replace_visitor.cpp
rename to src/library/replace_visitor.cpp
index 8ccd6e9d2..572f9ef33 100644
--- a/src/kernel/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include <tuple>
 #include "util/interrupt.h"
-#include "kernel/replace_visitor.h"
+#include "library/replace_visitor.h"
 
 namespace lean {
 expr replace_visitor::visit_sort(expr const & e) { lean_assert(is_sort(e)); return e; }
diff --git a/src/kernel/replace_visitor.h b/src/library/replace_visitor.h
similarity index 100%
rename from src/kernel/replace_visitor.h
rename to src/library/replace_visitor.h
diff --git a/src/library/tactic/tactic.cpp b/src/library/tactic/tactic.cpp
index 7458f9b3a..f4caaa25e 100644
--- a/src/library/tactic/tactic.cpp
+++ b/src/library/tactic/tactic.cpp
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
-#include "kernel/replace_visitor.h"
+#include "library/replace_visitor.h"
 #include "library/kernel_bindings.h"
 #include "library/tactic/tactic.h"
 #include "library/io_state_stream.h"