From d960c1994e5024ac9f923fe21647805c8ebdb44a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 15 Oct 2014 09:28:01 -0700 Subject: [PATCH] refactor(library/tactic/apply_tactic): reuse type_checker object --- src/library/tactic/apply_tactic.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/library/tactic/apply_tactic.cpp b/src/library/tactic/apply_tactic.cpp index 4569d6b6a7..28ae9f6fb6 100644 --- a/src/library/tactic/apply_tactic.cpp +++ b/src/library/tactic/apply_tactic.cpp @@ -29,7 +29,7 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const if (empty(gs)) return proof_state_seq(); name_generator ngen = s.get_ngen(); - std::unique_ptr tc = mk_type_checker(env, ngen.mk_child(), relax_main_opaque); + std::shared_ptr tc(mk_type_checker(env, ngen.mk_child(), relax_main_opaque)); goal g = head(gs); goals tail_gs = tail(gs); expr t = g.get_type(); @@ -73,9 +73,6 @@ static proof_state_seq apply_tactic_core(environment const & env, io_state const new_subst.assign(g.get_name(), new_p); goals new_gs = tail_gs; if (add_subgoals) { - // TODO(Leo): if mk_type_checker should return a shared_ptr, then we can reuse the tc defined - // before - std::unique_ptr tc = mk_type_checker(env, new_ngen.mk_child(), relax_main_opaque); buffer metas; for (auto m : meta_lst) { if (!new_subst.is_assigned(get_app_fn(m)))