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

fix(library/app_builder): missing initialization

Browse source
This commit is contained in:
Leonardo de Moura 2015-01-29 11:38:28 -08:00
parent 5bb2a41c64
commit 5efd91e435
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/app_builder.cpp
View file

@ -58,7 +58,9 @@ struct app_builder::imp {
cache m_cache;
buffer<levels> m_levels;
imp(type_checker & tc):m_tc(tc), m_plugin(mk_whnf_match_plugin(tc)) {}
imp(type_checker & tc):m_tc(tc), m_plugin(mk_whnf_match_plugin(tc)) {
m_levels.push_back(levels());
}
// Make sure m_levels contains at least nlvls metavariable universe levels
void ensure_levels(unsigned nlvls) {