diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 6a79b11f1..0783d0da4 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -7,7 +7,7 @@ begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp coercion_elaborator.cpp -proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp -builtin_tactics.cpp) +proof_qed_elaborator.cpp init_module.cpp elaborator_context.cpp) + target_link_libraries(lean_frontend ${LEAN_LIBS}) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index b43ac65da..7f194c2b6 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -16,7 +16,6 @@ Author: Leonardo de Moura #include "library/choice.h" #include "library/let.h" #include "frontends/lean/builtin_exprs.h" -#include "frontends/lean/builtin_tactics.h" #include "frontends/lean/token_table.h" #include "frontends/lean/calc.h" #include "frontends/lean/begin_end_ext.h" @@ -414,7 +413,6 @@ parse_table init_nud_table() { r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0); r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0); r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0); - init_nud_tactic_table(r); return r; } diff --git a/src/frontends/lean/builtin_tactics.cpp b/src/frontends/lean/builtin_tactics.cpp deleted file mode 100644 index 99b96ff1a..000000000 --- a/src/frontends/lean/builtin_tactics.cpp +++ /dev/null @@ -1,21 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "library/explicit.h" -#include "frontends/lean/parser.h" -#include "frontends/lean/parse_table.h" - -namespace lean { -void init_nud_tactic_table(parse_table & r) { -} - -void initialize_builtin_tactics() { -} - -void finalize_builtin_tactics() { -} -} diff --git a/src/frontends/lean/builtin_tactics.h b/src/frontends/lean/builtin_tactics.h deleted file mode 100644 index fd1fe6221..000000000 --- a/src/frontends/lean/builtin_tactics.h +++ /dev/null @@ -1,14 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "frontends/lean/parse_table.h" - -namespace lean { -void init_nud_tactic_table(parse_table & r); -void initialize_builtin_tactics(); -void finalize_builtin_tactics(); -} diff --git a/src/frontends/lean/init_module.cpp b/src/frontends/lean/init_module.cpp index f78b5fb3f..cc80e84cf 100644 --- a/src/frontends/lean/init_module.cpp +++ b/src/frontends/lean/init_module.cpp @@ -18,7 +18,6 @@ Author: Leonardo de Moura #include "frontends/lean/begin_end_ext.h" #include "frontends/lean/builtin_cmds.h" #include "frontends/lean/builtin_exprs.h" -#include "frontends/lean/builtin_tactics.h" #include "frontends/lean/inductive_cmd.h" #include "frontends/lean/structure_cmd.h" #include "frontends/lean/info_manager.h" @@ -34,7 +33,6 @@ void initialize_frontend_lean_module() { initialize_token_table(); initialize_parse_table(); initialize_builtin_cmds(); - initialize_builtin_tactics(); initialize_builtin_exprs(); initialize_elaborator_context(); initialize_elaborator(); @@ -73,7 +71,6 @@ void finalize_frontend_lean_module() { finalize_elaborator(); finalize_elaborator_context(); finalize_builtin_exprs(); - finalize_builtin_tactics(); finalize_builtin_cmds(); finalize_parse_table(); finalize_token_table();