From ed01242bc130c559453b045f931e567f81342371 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 May 2015 12:18:50 -0700 Subject: [PATCH] chore(library/tactic/apply_tactic): remove dead code --- src/library/tactic/apply_tactic.cpp | 6 ------ 1 file changed, 6 deletions(-) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 62e4bf0adc..d9a57e1e80 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -179,12 +179,6 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const }); } -static proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, - add_meta_kind add_meta, subgoals_action_kind subgoals_action, optional const & uk = optional()) { - buffer cs; - return apply_tactic_core(env, ios, s, e, cs, add_meta, subgoals_action, uk); -} - proof_state_seq apply_tactic_core(environment const & env, io_state const & ios, proof_state const & s, expr const & e, constraint_seq const & cs) { buffer tmp_cs; cs.linearize(tmp_cs);