From bb96f184ee22110e9856103146e26585f25b89d8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 8 Sep 2018 12:06:17 -0700 Subject: [PATCH] chore(library): remove dead code --- src/library/register_module.h | 38 ----------------------------------- 1 file changed, 38 deletions(-) delete mode 100644 src/library/register_module.h diff --git a/src/library/register_module.h b/src/library/register_module.h deleted file mode 100644 index bd32e80009..0000000000 --- a/src/library/register_module.h +++ /dev/null @@ -1,38 +0,0 @@ -/* -Copyright (c) 2013 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#pragma once -#include "util/script_state.h" -#include "library/kernel_bindings.h" -#include "library/resolve_macro.h" -#include "library/private.h" -#include "library/placeholder.h" -#include "library/aliases.h" -#include "library/choice.h" -#include "library/explicit.h" -#include "library/unifier.h" -#include "library/scoped_ext.h" -#include "library/match.h" -#include "library/reducible.h" - -namespace lean { -inline void open_core_module(lua_State * L) { - open_kernel_module(L); - open_resolve_macro(L); - open_private(L); - open_placeholder(L); - open_aliases(L); - open_choice(L); - open_scoped_ext(L); - open_unifier(L); - open_explicit(L); - open_match(L); - open_reducible(L); -} -inline void register_core_module() { - script_state::register_module(open_core_module); -} -}