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

fix(library/compiler/lambda_lifting): make sure auxiliary _lambda declarations come before the declarations that use them

Browse source 
This fixes a nasty initialization bug where an auxiliary `_closed`
declaration for an auxiliary `_lambda` is accessed before it is
initialized.
This commit is contained in:
Leonardo de Moura 2019-02-15 15:22:33 -08:00
parent 542bd432f8
commit 1080edd490
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/compiler/lambda_lifting.cpp
View file

@ -200,7 +200,8 @@ public:
m_base_name = cdecl.fst();
expr r = visit(cdecl.snd(), true);
comp_decl new_cdecl(cdecl.fst(), r);
return mk_pair(m_env, comp_decls(new_cdecl, comp_decls(m_new_decls)));
m_new_decls.push_back(new_cdecl);
return mk_pair(m_env, comp_decls(m_new_decls));
}
};