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

fix(library/blast/grind/intro_elim_lemmas): need to copy expr

Browse source
This commit is contained in:
Daniel Selsam 2016-01-21 17:09:34 -08:00 committed by Leonardo de Moura
parent d12067193b
commit 753d5d0689
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/grinder/intro_elim_lemmas.cpp
View file

@ -82,7 +82,7 @@ optional<name> get_intro_target(tmp_type_context & ctx, name const & c) {
expr local = ctx.mk_tmp_local(binding_domain(type));
type = ctx.try_to_pi(instantiate(binding_body(type), local));
}
expr const & fn = get_app_fn(ctx.whnf(type));
expr const fn = get_app_fn(ctx.whnf(type));
if (is_constant(fn))
return optional<name>(const_name(fn));
else