diff --git a/src/api/env.cpp b/src/api/env.cpp index 761c183267..177427ac5a 100644 --- a/src/api/env.cpp +++ b/src/api/env.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/environment.h" -#include "library/standard_kernel.h" +#include "kernel/standard_kernel.h" #include "library/module.h" #include "api/decl.h" #include "api/string.h" diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index d23cba946a..cb49b28193 100644 --- a/src/kernel/CMakeLists.txt +++ b/src/kernel/CMakeLists.txt @@ -3,4 +3,4 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp formatter.cpp declaration.cpp environment.cpp pos_info_provider.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp normalizer_extension.cpp init_module.cpp expr_cache.cpp -equiv_manager.cpp abstract_type_context.cpp) +equiv_manager.cpp abstract_type_context.cpp standard_kernel.cpp) diff --git a/src/library/standard_kernel.cpp b/src/kernel/standard_kernel.cpp similarity index 100% rename from src/library/standard_kernel.cpp rename to src/kernel/standard_kernel.cpp diff --git a/src/library/standard_kernel.h b/src/kernel/standard_kernel.h similarity index 100% rename from src/library/standard_kernel.h rename to src/kernel/standard_kernel.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 4133f5b9de..89e4f9c3d1 100644 --- a/src/library/CMakeLists.txt +++ b/src/library/CMakeLists.txt @@ -2,7 +2,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp io_state_stream.cpp bin_app.cpp constants.cpp kernel_serializer.cpp max_sharing.cpp shared_environment.cpp module.cpp private.cpp placeholder.cpp aliases.cpp - update_declaration.cpp scoped_ext.cpp standard_kernel.cpp sorry.cpp replace_visitor.cpp + update_declaration.cpp scoped_ext.cpp sorry.cpp replace_visitor.cpp explicit.cpp num.cpp string.cpp head_map.cpp class.cpp util.cpp print.cpp annotation.cpp quote.cpp typed_expr.cpp protected.cpp reducible.cpp init_module.cpp diff --git a/src/library/vm/vm_environment.cpp b/src/library/vm/vm_environment.cpp index 8ac9c3c981..49b1a451c1 100644 --- a/src/library/vm/vm_environment.cpp +++ b/src/library/vm/vm_environment.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/unfold_macros.h" #include "kernel/type_checker.h" #include "kernel/inductive/inductive.h" -#include "library/standard_kernel.h" +#include "kernel/standard_kernel.h" #include "library/module.h" #include "library/projection.h" #include "library/util.h" diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index e1d3ae0d33..d23c68d854 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -31,7 +31,7 @@ Author: Leonardo de Moura #include "library/st_task_queue.h" #include "library/mt_task_queue.h" #include "library/module_mgr.h" -#include "library/standard_kernel.h" +#include "kernel/standard_kernel.h" #include "library/module.h" #include "library/type_context.h" #include "library/io_state_stream.h" diff --git a/src/shell/lean_js.cpp b/src/shell/lean_js.cpp index 63778f0a0b..1a5bc7bb4e 100644 --- a/src/shell/lean_js.cpp +++ b/src/shell/lean_js.cpp @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include "library/module_mgr.h" #include "library/st_task_queue.h" #include "library/module.h" -#include "library/standard_kernel.h" +#include "kernel/standard_kernel.h" #include "library/type_context.h" #include "frontends/lean/pp.h" #include "frontends/lean/parser.h"