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

refactor(library/tactic/intros_tactic): change approach for generating fresh names for nameless 'intros'

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-26 21:27:09 -08:00
parent f7deabfd19
commit c2f32cd953
1 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/tactic/intros_tactic.cpp
View file

@ -22,7 +22,6 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
expr t = g.get_type();
expr m = g.get_meta();
bool gen_names = empty(ns);
unsigned nidx = 1;
try {
while (true) {
if (!gen_names && is_nil(ns))
@ -41,7 +40,7 @@ tactic intros_tactic(list<name> _ns, bool relax_main_opaque) {
new_name = head(ns);
ns = tail(ns);
} else {
new_name = g.get_unused_name(name("H"), nidx);
new_name = g.get_unused_name(binding_name(t));
}
expr new_local = mk_local(ngen.next(), new_name, binding_domain(t), binding_info(t));
t = instantiate(binding_body(t), new_local);