From 2f07bf352c53814addf072cc1189984d8a308280 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Sun, 22 Jan 2017 22:29:59 +0100
Subject: [PATCH] refactor(library/standard_kernel): move standard kernel into
 kernel

---
 src/api/env.cpp                             | 2 +-
 src/kernel/CMakeLists.txt                   | 2 +-
 src/{library => kernel}/standard_kernel.cpp | 0
 src/{library => kernel}/standard_kernel.h   | 0
 src/library/CMakeLists.txt                  | 2 +-
 src/library/vm/vm_environment.cpp           | 2 +-
 src/shell/lean.cpp                          | 2 +-
 src/shell/lean_js.cpp                       | 2 +-
 8 files changed, 6 insertions(+), 6 deletions(-)
 rename src/{library => kernel}/standard_kernel.cpp (100%)
 rename src/{library => kernel}/standard_kernel.h (100%)

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"