Rename import_all. The idea is to use consistent name for library files.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/CMakeLists.txt

@@ -95,8 +95,8 @@ add_subdirectory(library/arith)
 set(LEAN_LIBS ${LEAN_LIBS} arithlib)
 add_subdirectory(library/cast)
 set(LEAN_LIBS ${LEAN_LIBS} castlib)
-add_subdirectory(library/import_all)
-set(LEAN_LIBS ${LEAN_LIBS} import_all)
+add_subdirectory(library/all)
+set(LEAN_LIBS ${LEAN_LIBS} alllib)
 add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread ${LEAN_EXTRA_LINKER_FLAGS}")

src/frontends/lean/frontend.cpp

@@ -15,8 +15,8 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "kernel/environment.h"
 #include "library/expr_pair.h"
-#include "library/import_all/import_all.h"
 #include "library/state.h"
+#include "library/all/all.h"
 #include "frontends/lean/operator_info.h"
 #include "frontends/lean/coercion.h"
 #include "frontends/lean/frontend.h"

src/library/all/CMakeLists.txt

@@ -0,0 +1,2 @@
+add_library(alllib all.cpp)
+target_link_libraries(alllib ${LEAN_LIBS})

src/library/all/all.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
 #include "library/cast/cast.h"
-#include "library/import_all/import_all.h"
+#include "library/all/all.h"
 
 namespace lean {
 void import_all(environment & env) {

src/library/import_all/CMakeLists.txt

@@ -1,2 +0,0 @@
-add_library(import_all import_all.cpp)
-target_link_libraries(import_all ${LEAN_LIBS})

src/tests/frontends/lean/implicit_args.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "library/metavar.h"
 #include "library/printer.h"
 #include "library/basic_thms.h"
-#include "library/import_all/import_all.h"
+#include "library/all/all.h"
 #include "frontends/lean/frontend.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/elaborator_exception.h"

src/tests/kernel/arith.cpp

@@ -13,7 +13,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "library/printer.h"
 #include "library/arith/arith.h"
-#include "library/import_all/import_all.h"
+#include "library/all/all.h"
 using namespace lean;
 
 static void tst1() {

src/tests/kernel/environment.cpp

@@ -15,7 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "library/printer.h"
 #include "library/arith/arith.h"
-#include "library/import_all/import_all.h"
+#include "library/all/all.h"
 using namespace lean;
 
 static void tst1() {

src/tests/kernel/normalizer.cpp

@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/kernel_exception.h"
 #include "library/printer.h"
-#include "library/import_all/import_all.h"
+#include "library/all/all.h"
 using namespace lean;
 
 expr normalize(expr const & e) {

src/tests/kernel/threads.cpp

@@ -14,8 +14,8 @@ Author: Leonardo de Moura
 #include "kernel/normalizer.h"
 #include "library/max_sharing.h"
 #include "library/deep_copy.h"
-#include "library/import_all/import_all.h"
 #include "library/arith/arith.h"
+#include "library/all/all.h"
 using namespace lean;
 
 expr norm(expr const & e, environment & env) {

src/tests/kernel/type_checker.cpp

@@ -16,9 +16,9 @@ Author: Leonardo de Moura
 #include "kernel/builtin.h"
 #include "kernel/normalizer.h"
 #include "library/printer.h"
-#include "library/import_all/import_all.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
+#include "library/all/all.h"
 using namespace lean;
 
 expr c(char const * n) { return mk_constant(n); }

src/tests/library/light_checker.cpp

@@ -9,10 +9,10 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
-#include "library/arith/arith.h"
-#include "library/import_all/import_all.h"
 #include "library/light_checker.h"
 #include "library/printer.h"
+#include "library/arith/arith.h"
+#include "library/all/all.h"
 using namespace lean;
 
 static void tst1() {