From 04dfda99aba86ca1b190b4288c435c57495c195a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Nov 2014 14:51:12 -0800 Subject: [PATCH] fix(library/tactic/inversion_tactic): bug in name generation --- src/library/tactic/inversion_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/inversion_tactic.cpp b/src/library/tactic/inversion_tactic.cpp index 514b2500e9..a71a505a44 100644 --- a/src/library/tactic/inversion_tactic.cpp +++ b/src/library/tactic/inversion_tactic.cpp @@ -191,7 +191,7 @@ class inversion_tac { expr g_type = g.get_type(); for (unsigned i = 0; i < nargs; i++) { expr type = binding_domain(g_type); - expr new_h = mk_local(m_ngen.next(), get_unused_name(binding_name(g_type), hyps), type, binder_info()); + expr new_h = mk_local(m_ngen.next(), get_unused_name(binding_name(g_type), new_hyps), type, binder_info()); new_hyps.push_back(new_h); g_type = instantiate(binding_body(g_type), new_h); }