From 49698bd053f9a9a1f5d49a2a769c628e81d1687d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2013 13:37:25 -0800
Subject: [PATCH] chore(library/all): remove unnecessary files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/CMakeLists.txt                      |  2 --
 src/library/all/CMakeLists.txt          |  2 --
 src/library/all/all.cpp                 | 21 ---------------------
 src/library/all/all.h                   | 15 ---------------
 src/library/rewriter/fo_match.cpp       |  1 -
 src/tests/library/rewriter/fo_match.cpp |  1 -
 src/tests/library/rewriter/rewriter.cpp |  1 -
 7 files changed, 43 deletions(-)
 delete mode 100644 src/library/all/CMakeLists.txt
 delete mode 100644 src/library/all/all.cpp
 delete mode 100644 src/library/all/all.h

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 0acbea4de..907421c9f 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -213,8 +213,6 @@ add_subdirectory(library)
 set(LEAN_LIBS ${LEAN_LIBS} library)
 add_subdirectory(library/arith)
 set(LEAN_LIBS ${LEAN_LIBS} arithlib)
-add_subdirectory(library/all)
-set(LEAN_LIBS ${LEAN_LIBS} alllib)
 add_subdirectory(library/rewriter)
 set(LEAN_LIBS ${LEAN_LIBS} rewriter)
 add_subdirectory(library/elaborator)
diff --git a/src/library/all/CMakeLists.txt b/src/library/all/CMakeLists.txt
deleted file mode 100644
index e8499663b..000000000
--- a/src/library/all/CMakeLists.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-add_library(alllib all.cpp)
-target_link_libraries(alllib ${LEAN_LIBS})
diff --git a/src/library/all/all.cpp b/src/library/all/all.cpp
deleted file mode 100644
index 01056cf32..000000000
--- a/src/library/all/all.cpp
+++ /dev/null
@@ -1,21 +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
-*/
-#include "kernel/builtin.h"
-#include "library/arith/arith.h"
-#include "library/all/all.h"
-
-namespace lean {
-void import_all(environment const & env) {
-    import_kernel(env);
-    import_arith(env);
-}
-environment mk_toplevel() {
-    environment r;
-    import_all(r);
-    return r;
-}
-}
diff --git a/src/library/all/all.h b/src/library/all/all.h
deleted file mode 100644
index 40a5244ab..000000000
--- a/src/library/all/all.h
+++ /dev/null
@@ -1,15 +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 "kernel/environment.h"
-
-namespace lean {
-/** \brief Import all builtin libraries and theorems */
-void import_all(environment const & env);
-/** \brief Create top-level environment with all builtin libraries and theorems */
-environment mk_toplevel();
-}
diff --git a/src/library/rewriter/fo_match.cpp b/src/library/rewriter/fo_match.cpp
index 6164b2537..525073279 100644
--- a/src/library/rewriter/fo_match.cpp
+++ b/src/library/rewriter/fo_match.cpp
@@ -8,7 +8,6 @@ Author: Soonho Kong
 #include "util/trace.h"
 #include "kernel/expr.h"
 #include "kernel/printer.h"
-#include "library/all/all.h"
 #include "library/arith/nat.h"
 #include "library/arith/arith.h"
 #include "library/rewriter/fo_match.h"
diff --git a/src/tests/library/rewriter/fo_match.cpp b/src/tests/library/rewriter/fo_match.cpp
index bf59eba75..8d05ec6ed 100644
--- a/src/tests/library/rewriter/fo_match.cpp
+++ b/src/tests/library/rewriter/fo_match.cpp
@@ -11,7 +11,6 @@ Author: Soonho Kong
 #include "kernel/metavar.h"
 #include "kernel/printer.h"
 #include "kernel/builtin.h"
-#include "library/all/all.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"
 #include "library/rewriter/fo_match.h"
diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp
index 840d0eeca..6c8e056f6 100644
--- a/src/tests/library/rewriter/rewriter.cpp
+++ b/src/tests/library/rewriter/rewriter.cpp
@@ -12,7 +12,6 @@ Author: Soonho Kong
 #include "kernel/printer.h"
 #include "kernel/io_state.h"
 #include "kernel/builtin.h"
-#include "library/all/all.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"
 #include "library/rewriter/fo_match.h"