From a3d886f1e8bc16bf6dcdddb6e05f6249e99252be Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Sep 2018 08:51:21 -0700 Subject: [PATCH] chore(kernel/type_checker): remove leftover --- src/kernel/type_checker.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp index 852e2acf51..1e068b7223 100644 --- a/src/kernel/type_checker.cpp +++ b/src/kernel/type_checker.cpp @@ -73,8 +73,6 @@ expr type_checker::infer_fvar(expr const & e) { if (optional decl = m_lctx.find_local_decl(e)) { return decl->get_type(); } else { - // TODO(Leo): delete after we refactor inductive datatype module - return local_type(e); throw kernel_exception(m_env, "unknown free variable"); } }