From 5efd91e4353974500c2da890576700fff3d78f1e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 29 Jan 2015 11:38:28 -0800 Subject: [PATCH] fix(library/app_builder): missing initialization --- src/library/app_builder.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 97bd2138e2..3c5b323d78 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -58,7 +58,9 @@ struct app_builder::imp { cache m_cache; buffer 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) {