refactor(frontends/lean): move local_context to library

src/frontends/lean/CMakeLists.txt

@@ -4,8 +4,8 @@ parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
 server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
 inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
 begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
-theorem_queue.cpp structure_cmd.cpp info_manager.cpp info_annotation.cpp
-local_context.cpp choice_iterator.cpp find_cmd.cpp
+theorem_queue.cpp structure_cmd.cpp info_manager.cpp
+info_annotation.cpp choice_iterator.cpp find_cmd.cpp
 placeholder_elaborator.cpp coercion_elaborator.cpp info_tactic.cpp
 proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp
 calc_proof_elaborator.cpp type_util.cpp elaborator_exception.cpp)

src/frontends/lean/calc_proof_elaborator.cpp

@@ -10,8 +10,8 @@ Author: Leonardo de Moura
 #include "library/unifier.h"
 #include "library/reducible.h"
 #include "library/metavar_closure.h"
+#include "library/local_context.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/local_context.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/calc.h"
 #include "frontends/lean/calc_proof_elaborator.h"

src/frontends/lean/calc_proof_elaborator.h

@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <functional>
 #include "library/unifier.h"
+#include "library/local_context.h"
 #include "frontends/lean/info_manager.h"
-#include "frontends/lean/local_context.h"
 
 namespace lean {
 typedef std::function<void(expr const &)> update_type_info_fn;

src/frontends/lean/elaborator.cpp

@@ -30,16 +30,16 @@ Author: Leonardo de Moura
 #include "library/deep_copy.h"
 #include "library/metavar_closure.h"
 #include "library/typed_expr.h"
+#include "library/local_context.h"
 #include "library/tactic/expr_to_tactic.h"
 #include "library/error_handling/error_handling.h"
 #include "frontends/lean/local_decls.h"
 #include "frontends/lean/class.h"
 #include "frontends/lean/tactic_hint.h"
 #include "frontends/lean/info_manager.h"
-#include "frontends/lean/elaborator.h"
 #include "frontends/lean/info_annotation.h"
-#include "frontends/lean/local_context.h"
 #include "frontends/lean/choice_iterator.h"
+#include "frontends/lean/elaborator.h"
 #include "frontends/lean/placeholder_elaborator.h"
 #include "frontends/lean/proof_qed_elaborator.h"
 #include "frontends/lean/calc_proof_elaborator.h"

src/frontends/lean/elaborator.h

@@ -13,10 +13,10 @@ Author: Leonardo de Moura
 #include "library/expr_lt.h"
 #include "library/unifier.h"
 #include "library/tactic/tactic.h"
+#include "library/local_context.h"
 #include "frontends/lean/elaborator_context.h"
 #include "frontends/lean/coercion_elaborator.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/local_context.h"
 #include "frontends/lean/calc_proof_elaborator.h"
 
 namespace lean {

src/frontends/lean/placeholder_elaborator.cpp

@@ -16,8 +16,8 @@ Author: Leonardo de Moura
 #include "library/metavar_closure.h"
 #include "library/error_handling/error_handling.h"
 #include "library/class.h"
+#include "library/local_context.h"
 #include "frontends/lean/util.h"
-#include "frontends/lean/local_context.h"
 #include "frontends/lean/choice_iterator.h"
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/pp_options.h"

src/frontends/lean/placeholder_elaborator.h

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "library/io_state.h"
-#include "frontends/lean/local_context.h"
+#include "library/local_context.h"
 
 namespace lean {
 /** \brief Create a metavariable, and attach choice constraint for generating

src/library/CMakeLists.txt

@@ -10,6 +10,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   definition_cache.cpp declaration_index.cpp class.cpp util.cpp
   print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
   protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp
-  fingerprint.cpp flycheck.cpp hott_kernel.cpp)
+  fingerprint.cpp flycheck.cpp hott_kernel.cpp local_context.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/local_context.cpp

@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/replace_fn.h"
 #include "kernel/metavar.h"
-#include "frontends/lean/local_context.h"
+#include "library/local_context.h"
 
 namespace lean {
 /** \brief Given a list of local constants \c locals