From 894875dc5c49bab6e48a5dba3bf7259fe5591f54 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 13 Dec 2015 15:03:25 -0800 Subject: [PATCH] feat(library/tactic/congruence_tactic): closes #855 --- src/library/tactic/congruence_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/tactic/congruence_tactic.cpp b/src/library/tactic/congruence_tactic.cpp index f10bad0a19..14da37b912 100644 --- a/src/library/tactic/congruence_tactic.cpp +++ b/src/library/tactic/congruence_tactic.cpp @@ -79,7 +79,7 @@ optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios if (ss[i]) { arg_kinds.push_back(congr_arg_kind::Singleton); expr new_type = replace_locals(mlocal_type(d_i), rhss, lhss); - expr new_d_i = mk_local(get_unused_name(name(local_pp_name(d_i), "new"), hyps), new_type); + expr new_d_i = mk_local(get_unused_name(local_pp_name(d_i).append_after("new"), hyps), new_type); hyps.push_back(new_d_i); rhss.push_back(d_i); lhss.push_back(new_d_i); @@ -99,7 +99,7 @@ optional mk_congr_subsingleton_thm(type_checker & tc, io_state const & ios } else { arg_kinds.push_back(congr_arg_kind::Eq); expr new_type = replace_locals(mlocal_type(d_i), rhss, lhss); - expr new_d_i = mk_local(get_unused_name(name(local_pp_name(d_i), "new"), hyps), new_type); + expr new_d_i = mk_local(get_unused_name(local_pp_name(d_i).append_after("new"), hyps), new_type); name new_h_name = get_unused_name(name(h, eqidx), hyps); eqidx++; expr new_eq = mk_local(new_h_name, mk_eq(tc, new_d_i, d_i));