diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 1707661032..176128d118 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -339,6 +339,8 @@ add_subdirectory(library/tactic/backward)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:backward>)
 add_subdirectory(library/constructions)
 set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
+add_subdirectory(library/equations_compiler)
+set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:equations_compiler>)
 # add_subdirectory(library/blast)
 # set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:blast>)
 # add_subdirectory(library/blast/backward)
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 34a4da785c..9ff3c2312a 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -20,7 +20,7 @@ Author: Leonardo de Moura
 #include "library/string.h"
 #include "library/trace.h"
 #include "library/tactic/elaborate.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/builtin_exprs.h"
 #include "frontends/lean/decl_cmds.h"
 #include "frontends/lean/token_table.h"
diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 73d9614602..3ed45148c8 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -24,7 +24,7 @@ Author: Leonardo de Moura
 #include "library/abbreviation.h"
 #include "library/flycheck.h"
 #include "library/error_handling.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/vm/vm.h"
diff --git a/src/frontends/lean/match_expr.cpp b/src/frontends/lean/match_expr.cpp
index 1ea39e3362..2db867473e 100644
--- a/src/frontends/lean/match_expr.cpp
+++ b/src/frontends/lean/match_expr.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "util/fresh_name.h"
 #include "kernel/abstract.h"
 #include "library/placeholder.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser.h"
diff --git a/src/frontends/lean/old_elaborator.cpp b/src/frontends/lean/old_elaborator.cpp
index 97c4aac06d..47b850a625 100644
--- a/src/frontends/lean/old_elaborator.cpp
+++ b/src/frontends/lean/old_elaborator.cpp
@@ -43,7 +43,7 @@ Author: Leonardo de Moura
 #include "library/class_instance_resolution.h"
 #include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "library/compiler/rec_fn_macro.h"
 #include "library/compiler/vm_compiler.h"
 #include "library/vm/vm.h"
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 19a7a31e1a..c7f1232759 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -46,7 +46,7 @@ Author: Leonardo de Moura
 #include "library/error_handling.h"
 #include "library/scope_pos_info_provider.h"
 #include "library/legacy_type_context.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "frontends/lean/tokens.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 0de3824afb..8bd031060a 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -37,7 +37,7 @@ Author: Leonardo de Moura
 #include "library/string.h"
 #include "library/type_context.h"
 #include "library/idx_metavar.h"
-#include "library/constructions/equations.h"
+#include "library/equations_compiler/equations.h"
 #include "library/tactic/tactic_state.h"
 #include "library/compiler/comp_irrelevant.h"
 #include "library/compiler/erase_irrelevant.h"
diff --git a/src/frontends/lean/type_util.h b/src/frontends/lean/type_util.h
index 58b66daf04..b529e16f59 100644
--- a/src/frontends/lean/type_util.h
+++ b/src/frontends/lean/type_util.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "library/old_util.h"
+#include "library/util.h"
 
 namespace lean {
 class parser;
diff --git a/src/library/constructions/CMakeLists.txt b/src/library/constructions/CMakeLists.txt
index 4f5c0aab0c..0cd5d6bce6 100644
--- a/src/library/constructions/CMakeLists.txt
+++ b/src/library/constructions/CMakeLists.txt
@@ -1,5 +1,2 @@
 add_library(constructions OBJECT rec_on.cpp induction_on.cpp cases_on.cpp
-  no_confusion.cpp projection.cpp brec_on.cpp equations.cpp
-  init_module.cpp
-#LEGACY
-  old_goal.cpp old_inversion.cpp)
+  no_confusion.cpp projection.cpp brec_on.cpp init_module.cpp)
diff --git a/src/library/constructions/init_module.cpp b/src/library/constructions/init_module.cpp
index 13d2b35b36..028d878b14 100644
--- a/src/library/constructions/init_module.cpp
+++ b/src/library/constructions/init_module.cpp
@@ -4,18 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/old_util.h"
-#include "library/constructions/equations.h"
 #include "library/constructions/projection.h"
 
 namespace lean{
 void initialize_constructions_module() {
-    initialize_equations();
     initialize_def_projection();
 }
 
 void finalize_constructions_module() {
     finalize_def_projection();
-    finalize_equations();
 }
 }
diff --git a/src/library/constructions/projection.h b/src/library/constructions/projection.h
index 4194b3722c..73e79a6431 100644
--- a/src/library/constructions/projection.h
+++ b/src/library/constructions/projection.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include "kernel/environment.h"
+#include "library/util.h"
 
 namespace lean {
 /** \brief Create projections operators for the structure named \c n.
diff --git a/src/library/constructions/equations.cpp b/src/library/equations_compiler/equations.cpp
similarity index 99%
rename from src/library/constructions/equations.cpp
rename to src/library/equations_compiler/equations.cpp
index 09649938a2..43c8f5b6c1 100644
--- a/src/library/constructions/equations.cpp
+++ b/src/library/equations_compiler/equations.cpp
@@ -27,7 +27,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/normalize.h"
 #include "library/pp_options.h"
-#include "library/constructions/old_inversion.h"
+#include "library/equations_compiler/old_inversion.h"
 
 namespace lean {
 static name * g_equations_name                 = nullptr;
diff --git a/src/library/constructions/equations.h b/src/library/equations_compiler/equations.h
similarity index 100%
rename from src/library/constructions/equations.h
rename to src/library/equations_compiler/equations.h
diff --git a/src/library/constructions/old_goal.cpp b/src/library/equations_compiler/old_goal.cpp
similarity index 99%
rename from src/library/constructions/old_goal.cpp
rename to src/library/equations_compiler/old_goal.cpp
index 2378b0e5b3..9856ade81a 100644
--- a/src/library/constructions/old_goal.cpp
+++ b/src/library/equations_compiler/old_goal.cpp
@@ -16,7 +16,7 @@ Author: Leonardo de Moura
 #include "library/metavar.h"
 #include "library/util.h"
 #include "library/old_util.h"
-#include "library/constructions/old_goal.h"
+#include "library/equations_compiler/old_goal.h"
 
 namespace lean {
 old_local_context old_goal::to_local_context() const {
diff --git a/src/library/constructions/old_goal.h b/src/library/equations_compiler/old_goal.h
similarity index 100%
rename from src/library/constructions/old_goal.h
rename to src/library/equations_compiler/old_goal.h
diff --git a/src/library/constructions/old_inversion.cpp b/src/library/equations_compiler/old_inversion.cpp
similarity index 99%
rename from src/library/constructions/old_inversion.cpp
rename to src/library/equations_compiler/old_inversion.cpp
index 2309e75c7a..bb265510d4 100644
--- a/src/library/constructions/old_inversion.cpp
+++ b/src/library/equations_compiler/old_inversion.cpp
@@ -17,7 +17,7 @@ Author: Leonardo de Moura
 #include "library/constants.h"
 #include "library/reducible.h"
 #include "library/class_instance_resolution.h"
-#include "library/constructions/old_inversion.h"
+#include "library/equations_compiler/old_inversion.h"
 
 namespace lean {
 namespace inversion {
diff --git a/src/library/constructions/old_inversion.h b/src/library/equations_compiler/old_inversion.h
similarity index 98%
rename from src/library/constructions/old_inversion.h
rename to src/library/equations_compiler/old_inversion.h
index ff956bdb51..72a352750a 100644
--- a/src/library/constructions/old_inversion.h
+++ b/src/library/equations_compiler/old_inversion.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "kernel/expr.h"
 #include "library/metavar.h"
-#include "library/constructions/old_goal.h"
+#include "library/equations_compiler/old_goal.h"
 
 
 namespace lean {
diff --git a/src/library/old_util.cpp b/src/library/old_util.cpp
index ad5164210d..02bced52d7 100644
--- a/src/library/old_util.cpp
+++ b/src/library/old_util.cpp
@@ -262,22 +262,6 @@ bool is_some(expr const & e, expr & A, expr & a) {
     }
 }
 
-expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) {
-    switch (k) {
-    case implicit_infer_kind::Implicit: {
-        bool strict = true;
-        return infer_implicit(type, nparams, strict);
-    }
-    case implicit_infer_kind::RelaxedImplicit: {
-        bool strict = false;
-        return infer_implicit(type, nparams, strict);
-    }
-    case implicit_infer_kind::None:
-        return type;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
 bool has_expr_metavar_relaxed(expr const & e) {
     if (!has_expr_metavar(e))
         return false;
diff --git a/src/library/old_util.h b/src/library/old_util.h
index bbeaa9b4f9..f683bc221b 100644
--- a/src/library/old_util.h
+++ b/src/library/old_util.h
@@ -70,13 +70,6 @@ bool is_none(expr const & e, expr & A);
 /** \brief Return true iff \c e is of the form (@option.some A a), and update \c A and \c a */
 bool is_some(expr const & e, expr & A, expr & a);
 
-enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
-
-/** \brief Infer implicit parameter annotations for the first \c nparams using mode
-    specified by \c k.
-*/
-expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
-
 /** \brief Similar to has_expr_metavar, but ignores metavariables occurring in the type
     of local constants */
 bool has_expr_metavar_relaxed(expr const & e);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index d14040d8d7..63d93b858b 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -909,6 +909,22 @@ expr beta_eta_reduce(expr t) {
     return eta_beta_reduce_fn<true, true>()(t);
 }
 
+expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k) {
+    switch (k) {
+    case implicit_infer_kind::Implicit: {
+        bool strict = true;
+        return infer_implicit(type, nparams, strict);
+    }
+    case implicit_infer_kind::RelaxedImplicit: {
+        bool strict = false;
+        return infer_implicit(type, nparams, strict);
+    }
+    case implicit_infer_kind::None:
+        return type;
+    }
+    lean_unreachable(); // LCOV_EXCL_LINE
+}
+
 void initialize_library_util() {
     g_true           = new expr(mk_constant(get_true_name()));
     g_true_intro     = new expr(mk_constant(get_true_intro_name()));
diff --git a/src/library/util.h b/src/library/util.h
index ab6a1ae19c..2f6ffae77f 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -229,6 +229,12 @@ expr beta_reduce(expr t);
 expr eta_reduce(expr t);
 expr beta_eta_reduce(expr t);
 
+enum class implicit_infer_kind { Implicit, RelaxedImplicit, None };
+
+/** \brief Infer implicit parameter annotations for the first \c nparams using mode
+    specified by \c k. */
+expr infer_implicit_params(expr const & type, unsigned nparams, implicit_infer_kind k);
+
 void initialize_library_util();
 void finalize_library_util();
 }