chore(frontends/lean/definition_cmds): update comment

This commit is contained in:
Leonardo de Moura 2016-12-08 10:35:32 -08:00
parent 716502c502
commit e01c7bfef5

View file

@ -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);