diff --git a/library/hott/Makefile b/library/hott/Makefile
deleted file mode 100644
index 20770a207..000000000
--- a/library/hott/Makefile
+++ /dev/null
@@ -1,2 +0,0 @@
-include ../Makefile.common
-LEAN_OPTIONS+=--hott
diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt
index 6cabe00f8..78400443a 100644
--- a/src/shell/CMakeLists.txt
+++ b/src/shell/CMakeLists.txt
@@ -75,15 +75,6 @@ FOREACH(T ${LEANSLOWTESTS})
   set_tests_properties("leanslowtest_${T_NAME}" PROPERTIES LABELS "expensive")
 ENDFOREACH(T)
 
-# LEAN HoTT TESTS
-file(GLOB LEANHOTTTESTS "${LEAN_SOURCE_DIR}/../tests/lean/hott/*.lean")
-FOREACH(T ${LEANHOTTTESTS})
-  GET_FILENAME_COMPONENT(T_NAME ${T} NAME)
-  add_test(NAME "leanhotttest_${T_NAME}"
-           WORKING_DIRECTORY "${LEAN_SOURCE_DIR}/../tests/lean/hott"
-           COMMAND "./test_single.sh" "${CMAKE_CURRENT_BINARY_DIR}/lean" ${T_NAME})
-ENDFOREACH(T)
-
 # LEAN LUA TESTS
 file(GLOB LEANLUATESTS "${LEAN_SOURCE_DIR}/../tests/lua/*.lua")
 FOREACH(T ${LEANLUATESTS})
diff --git a/tests/lean/hott/uuu.lean b/tests/lean/run/uuu.lean
similarity index 100%
rename from tests/lean/hott/uuu.lean
rename to tests/lean/run/uuu.lean