From ffc5ccf11885bf8b22fb47cc798f78a2a546c014 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 28 Oct 2020 05:47:37 -0700
Subject: [PATCH] chore: remove dead code

---
 src/library/CMakeLists.txt   |  2 +-
 src/library/check.cpp        | 30 ------------------------------
 src/library/check.h          | 20 --------------------
 src/library/init_module.cpp  |  3 ---
 src/library/type_context.cpp |  1 -
 5 files changed, 1 insertion(+), 55 deletions(-)
 delete mode 100644 src/library/check.cpp
 delete mode 100644 src/library/check.h

diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 7e12c55b6f..9c85cc6d1d 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -6,7 +6,7 @@ add_library(library OBJECT expr_lt.cpp io_state.cpp
   pp_options.cpp projection.cpp
   aux_recursors.cpp trace.cpp
   type_context.cpp
-  locals.cpp messages.cpp message_builder.cpp check.cpp
+  locals.cpp messages.cpp message_builder.cpp
   profiling.cpp time_task.cpp
   scope_pos_info_provider.cpp formatter.cpp json.cpp
   pos_info_provider.cpp abstract_type_context.cpp)
diff --git a/src/library/check.cpp b/src/library/check.cpp
deleted file mode 100644
index 8b35b9b184..0000000000
--- a/src/library/check.cpp
+++ /dev/null
@@ -1,30 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/expr_sets.h"
-#include "kernel/instantiate.h"
-#include "library/trace.h"
-#include "library/type_context.h"
-
-namespace lean {
-struct check_fn {
-    type_context_old &   m_ctx;
-    expr_set             m_visited;
-public:
-    check_fn(type_context_old & ctx):m_ctx(ctx) {}
-};
-
-void check(type_context_old &, expr const &) {
-    lean_unreachable();
-}
-
-void initialize_check() {
-    register_trace_class("check");
-}
-
-void finalize_check() {
-}
-}
diff --git a/src/library/check.h b/src/library/check.h
deleted file mode 100644
index e9e02f2f02..0000000000
--- a/src/library/check.h
+++ /dev/null
@@ -1,20 +0,0 @@
-/*
-Copyright (c) 2017 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include "library/type_context.h"
-
-namespace lean {
-/* Type check 'e' using the given type context.
-   It throws an exception in case of failure.
-
-   This procedure is use to check the proof-term produced by tactics such as
-   rewrite.
-*/
-void check(type_context_old & ctx, expr const & e);
-void initialize_check();
-void finalize_check();
-}
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 80a9c7ea69..53788852a0 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -16,7 +16,6 @@ Author: Leonardo de Moura
 #include "library/util.h"
 #include "library/pp_options.h"
 #include "library/type_context.h"
-#include "library/check.h"
 #include "library/profiling.h"
 #include "library/time_task.h"
 #include "library/formatter.h"
@@ -49,13 +48,11 @@ void initialize_library_module() {
     initialize_library_util();
     initialize_pp_options();
     initialize_type_context();
-    initialize_check();
     initialize_time_task();
 }
 
 void finalize_library_module() {
     finalize_time_task();
-    finalize_check();
     finalize_type_context();
     finalize_pp_options();
     finalize_library_util();
diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 9110b17715..fccba95bea 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -26,7 +26,6 @@ Author: Leonardo de Moura
 #include "library/locals.h"
 #include "library/aux_recursors.h"
 #include "library/num.h"
-#include "library/check.h"
 #include "library/time_task.h"
 
 namespace lean {