From e01c7bfef54c01986e5bc8d5351767dffa767e82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Dec 2016 10:35:32 -0800 Subject: [PATCH] chore(frontends/lean/definition_cmds): update comment --- src/frontends/lean/definition_cmds.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/definition_cmds.cpp b/src/frontends/lean/definition_cmds.cpp index 2b4d6d7690..04f9120159 100644 --- a/src/frontends/lean/definition_cmds.cpp +++ b/src/frontends/lean/definition_cmds.cpp @@ -629,7 +629,7 @@ public: throw exception("not a rfl-lemma, even though marked as rfl"); return inline_new_defs(m_decl_env, elab.env(), val); } catch (exception & ex) { - // TODO(gabriel,leo): remove this catch block after single threaded queue discard bad tasks + /* Remark: we need the catch to be able to produce correct line information */ message_builder error_msg(&m_pos_provider, tc, m_decl_env, get_global_ios(), m_pos_provider.get_file_name(), m_pos_provider.get_some_pos(), ERROR);