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 #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"