max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/compiler/emit_cpp): collect_dependencies was not handling _closure instruction

Browse source
This commit is contained in:
Leonardo de Moura 2019-01-29 16:31:29 -08:00
parent 20641731e3
commit e4c4eab48e
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/compiler/emit_cpp.cpp
View file

@ -194,6 +194,10 @@ static void collect_dependencies(environment const & env, expr e, name_set & dep
get_app_args(e, args);
for (expr const & arg : args)
collect_dependencies(env, arg, deps);
} else if (is_llnf_closure(get_app_fn(e))) {
buffer<expr> args;
get_app_args(e, args);
collect_constant(args[0], deps);
} else {
collect_constant(get_app_fn(e), deps);
}