From f464775af6ee0baf008c4e3dbd2855bdd304808d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 2 Jul 2014 08:36:25 -0700 Subject: [PATCH] fix(frontends/lean/parser): bug when parsing identifiers Signed-off-by: Leonardo de Moura --- src/frontends/lean/parser.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index c2f54290a5..d433efa396 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -832,7 +832,7 @@ expr parser::id_to_expr(name const & id, pos_info const & p) { } r = save_pos(mk_choice(new_as.size(), new_as.data()), p); } - if (m_no_undef_id_error) + if (!r && m_no_undef_id_error) r = save_pos(mk_constant(get_namespace(m_env) + id, ls), p); if (!r) throw parser_error(sstream() << "unknown identifier '" << id << "'", p);