diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 0462569bc2..222202b1de 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -12,7 +12,6 @@ add_library(
   util.cpp
   print.cpp
   annotation.cpp
-  reducible.cpp
   init_module.cpp
   profiling.cpp
   time_task.cpp
diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp
index 90f24bfb11..362b1933e3 100644
--- a/src/library/constructions/cases_on.cpp
+++ b/src/library/constructions/cases_on.cpp
@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/inductive.h"
 #include "library/suffixes.h"
-#include "library/reducible.h"
+#include "library/util.h"
 #include "library/constants.h"
 #include "library/constructions/util.h"
 
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
deleted file mode 100644
index a2f009f640..0000000000
--- a/src/library/reducible.cpp
+++ /dev/null
@@ -1,24 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <string>
-#include "library/elab_environment.h"
-#include "library/reducible.h"
-
-namespace lean {
-extern "C" uint8 lean_get_reducibility_status(object * env, object * n);
-extern "C" object * lean_set_reducibility_status(object * env, object * n, uint8 s);
-
-elab_environment set_reducible(elab_environment const & env, name const & n, reducible_status s, bool persistent) {
-    if (!persistent)
-        throw exception("reducibility attributes must be persistent for now, we will relax this restriction in a near future");
-    return elab_environment(lean_set_reducibility_status(env.to_obj_arg(), n.to_obj_arg(), static_cast<uint8>(s)));
-}
-
-reducible_status get_reducible_status(elab_environment const & env, name const & n) {
-    return static_cast<reducible_status>(lean_get_reducibility_status(env.to_obj_arg(), n.to_obj_arg()));
-}
-}
diff --git a/src/library/reducible.h b/src/library/reducible.h
deleted file mode 100644
index f1fa9e44d2..0000000000
--- a/src/library/reducible.h
+++ /dev/null
@@ -1,30 +0,0 @@
-/*
-Copyright (c) 2014 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <memory>
-#include "library/util.h"
-#include "library/elab_environment.h"
-
-namespace lean {
-enum class reducible_status { Reducible, Semireducible, Irreducible };
-/** \brief Mark the definition named \c n as reducible or not.
-
-    The method throws an exception if \c n is
-      - not a definition
-      - a theorem
-      - an opaque definition that was not defined in main module
-
-    "Reducible" definitions can be freely unfolded by automation (i.e., elaborator, simplifier, etc).
-    We should view it as a hint to automation.
-*/
-elab_environment set_reducible(elab_environment const & env, name const & n, reducible_status s, bool persistent);
-
-reducible_status get_reducible_status(elab_environment const & env, name const & n);
-
-inline bool is_reducible(elab_environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Reducible; }
-inline bool is_semireducible(elab_environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Semireducible; }
-}