From 56a81eda6e28dccdb3b9814a4a4037872956b6c2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 15 Aug 2014 16:37:24 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): uninit variable Signed-off-by: Leonardo de Moura --- src/frontends/lean/elaborator.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 92439052e..e41fa1bca 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -520,8 +520,9 @@ public: m_context(m_ngen, m_mvar2meta, ctx), m_full_context(m_ngen, m_mvar2meta, ctx) { m_relax_main_opaque = false; - m_tc[0] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), false); - m_tc[1] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), true); + m_noinfo = false; + m_tc[0] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), false); + m_tc[1] = mk_type_checker_with_hints(env.m_env, m_ngen.mk_child(), true); } environment const & env() const { return m_env.m_env; }