From bb1c6d44ac274998ba04919f18b2f7d0972949f6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 25 Sep 2014 17:52:36 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): missing register_meta --- src/frontends/lean/elaborator.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index a251cb28f..df5249990 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -266,6 +266,7 @@ public: auto ec = mk_placeholder_elaborator(env(), ios(), m_context, m_ngen.next(), m_relax_main_opaque, use_local_instances(), is_strict, type, g, m_unifier_config); + register_meta(ec.first); cs += ec.second; return ec.first; }