From c60b5948396c050f81858ed509d79d68d4f9cbcc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Jan 2018 15:18:58 -0800 Subject: [PATCH] chore(library/type_context): remove unnecessary #include --- src/library/type_context.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 031c985d88..f6b8e891f8 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -32,8 +32,6 @@ Author: Leonardo de Moura #include "library/fun_info.h" #include "library/num.h" #include "library/quote.h" -// TODO(Leo): move rec_fn_macro to library -#include "library/compiler/rec_fn_macro.h" #ifndef LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH #define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32