michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tactic): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-16 11:57:37 -07:00
parent 0dc674e350
commit 169f956143
3 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tactic/apply_tactic.cpp
View file

@ -223,11 +223,6 @@ tactic eapply_tactic(elaborate_fn const & elab, expr const & e) {
return apply_tactic_core(elab, e, AddAll, AddSubgoals); return apply_tactic_core(elab, e, AddAll, AddSubgoals);
} }
int mk_eassumption_tactic(lua_State * L) { return push_tactic(L, eassumption_tactic()); }
void open_apply_tactic(lua_State * L) {
SET_GLOBAL_FUN(mk_eassumption_tactic, "eassumption_tac");
}
void initialize_apply_tactic() { void initialize_apply_tactic() {
g_apply_class_instance = new name{"apply", "class_instance"}; g_apply_class_instance = new name{"apply", "class_instance"};
register_bool_option(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE, register_bool_option(*g_apply_class_instance, LEAN_DEFAULT_APPLY_CLASS_INSTANCE,

1
src/library/tactic/apply_tactic.h
View file

@ -14,7 +14,6 @@ tactic apply_tactic(elaborate_fn const & fn, expr const & e);
tactic fapply_tactic(elaborate_fn const & fn, expr const & e); tactic fapply_tactic(elaborate_fn const & fn, expr const & e);
tactic eassumption_tactic(); tactic eassumption_tactic();
tactic assumption_tactic(); tactic assumption_tactic();
void open_apply_tactic(lua_State * L);
void initialize_apply_tactic(); void initialize_apply_tactic();
void finalize_apply_tactic(); void finalize_apply_tactic();
} }

2
src/library/tactic/register_module.h
View file

@ -9,7 +9,6 @@ Author: Leonardo de Moura
#include "library/tactic/goal.h" #include "library/tactic/goal.h"
#include "library/tactic/proof_state.h" #include "library/tactic/proof_state.h"
#include "library/tactic/tactic.h" #include "library/tactic/tactic.h"
#include "library/tactic/apply_tactic.h"
// #include "library/tactic/simplify_tactic.h" // #include "library/tactic/simplify_tactic.h"
namespace lean { namespace lean {
@ -17,7 +16,6 @@ inline void open_tactic_module(lua_State * L) {
open_goal(L); open_goal(L);
open_proof_state(L); open_proof_state(L);
open_tactic(L); open_tactic(L);
open_apply_tactic(L);
// open_simplify_tactic(L); // open_simplify_tactic(L);
} }
inline void register_tactic_module() { inline void register_tactic_module() {