diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt index 7cb0ce7e14..df179a6559 100644 --- a/src/library/compiler/CMakeLists.txt +++ b/src/library/compiler/CMakeLists.txt @@ -4,5 +4,5 @@ add_library(compiler OBJECT old_util.cpp eta_expansion.cpp preprocess.cpp lambda_lifting.cpp simp_inductive.cpp nat_value.cpp vm_compiler.cpp old_cse.cpp elim_unused_lets.cpp extract_values.cpp init_module.cpp ## New compiler - lc_util.cpp lcnf.cpp csimp.cpp elim_dead_let.cpp cse.cpp + util.cpp lcnf.cpp csimp.cpp elim_dead_let.cpp cse.cpp ) diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp index b60e17eb46..69715f050c 100644 --- a/src/library/compiler/cse.cpp +++ b/src/library/compiler/cse.cpp @@ -10,7 +10,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "kernel/abstract.h" #include "kernel/expr_maps.h" -#include "library/compiler/lc_util.h" +#include "library/compiler/util.h" namespace lean { static name * g_cse_fresh = nullptr; diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 6b22939373..27d11e63fc 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -9,7 +9,7 @@ Author: Leonardo de Moura #include "kernel/instantiate.h" #include "library/util.h" #include "library/constants.h" -#include "library/compiler/lc_util.h" +#include "library/compiler/util.h" namespace lean { class csimp_fn { diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp index 42f47f0437..e38bdf0c6c 100644 --- a/src/library/compiler/lcnf.cpp +++ b/src/library/compiler/lcnf.cpp @@ -6,6 +6,7 @@ Author: Leonardo de Moura */ #include #include "runtime/flet.h" +#include "runtime/sstream.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" #include "library/expr_lt.h" @@ -13,10 +14,7 @@ Author: Leonardo de Moura #include "library/aux_recursors.h" #include "library/constants.h" #include "library/projection.h" -#include "library/compiler/lc_util.h" - -#include "library/trace.h" -#include "kernel/for_each_fn.h" +#include "library/compiler/util.h" namespace lean { class to_lcnf_fn { diff --git a/src/library/compiler/preprocess.cpp b/src/library/compiler/preprocess.cpp index 0a22226311..51da8061ac 100644 --- a/src/library/compiler/preprocess.cpp +++ b/src/library/compiler/preprocess.cpp @@ -36,7 +36,7 @@ Author: Leonardo de Moura #include "library/compiler/extract_values.h" #include "library/compiler/old_cse.h" -#include "library/compiler/lc_util.h" +#include "library/compiler/util.h" #include "library/compiler/lcnf.h" #include "library/compiler/csimp.h" #include "library/compiler/elim_dead_let.h" diff --git a/src/library/compiler/lc_util.cpp b/src/library/compiler/util.cpp similarity index 100% rename from src/library/compiler/lc_util.cpp rename to src/library/compiler/util.cpp diff --git a/src/library/compiler/lc_util.h b/src/library/compiler/util.h similarity index 100% rename from src/library/compiler/lc_util.h rename to src/library/compiler/util.h