From bd3efca5e95340399aabc660191df40585d40345 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Mar 2016 09:57:31 -0700
Subject: [PATCH] chore(library/CMakeFiles): make clear which files should be
 deleted after refactoring

---
 src/library/CMakeLists.txt | 32 ++++++++++++++------------------
 1 file changed, 14 insertions(+), 18 deletions(-)

diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 8dec7eed40..8bf6359cf0 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,28 +1,24 @@
 add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
-  io_state_stream.cpp bin_app.cpp
-  constants.cpp kernel_serializer.cpp
-  max_sharing.cpp normalize.cpp shared_environment.cpp module.cpp
+  io_state_stream.cpp bin_app.cpp constants.cpp kernel_serializer.cpp
+  max_sharing.cpp shared_environment.cpp module.cpp
   coercion.cpp private.cpp placeholder.cpp aliases.cpp level_names.cpp
-  update_declaration.cpp choice.cpp scoped_ext.cpp locals.cpp
-  standard_kernel.cpp sorry.cpp replace_visitor.cpp unifier.cpp
-  explicit.cpp num.cpp
-  string.cpp head_map.cpp match.cpp definition_cache.cpp
+  update_declaration.cpp scoped_ext.cpp standard_kernel.cpp sorry.cpp replace_visitor.cpp
+  explicit.cpp num.cpp string.cpp head_map.cpp definition_cache.cpp
   declaration_index.cpp class.cpp util.cpp print.cpp annotation.cpp
-  typed_expr.cpp let.cpp protected.cpp
-  metavar_closure.cpp reducible.cpp init_module.cpp
-  generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp
-  old_local_context.cpp choice_iterator.cpp pp_options.cpp
+  typed_expr.cpp protected.cpp reducible.cpp init_module.cpp
+  generic_exception.cpp fingerprint.cpp flycheck.cpp hott_kernel.cpp pp_options.cpp
   unfold_macros.cpp app_builder.cpp projection.cpp abbreviation.cpp
   relation_manager.cpp export.cpp user_recursors.cpp idx_metavar.cpp
   composition_manager.cpp tc_multigraph.cpp noncomputable.cpp
-  aux_recursors.cpp norm_num.cpp norm_num.cpp class_instance_resolution.cpp old_type_context.cpp
-  tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
+  aux_recursors.cpp norm_num.cpp fun_info_manager.cpp congr_lemma_manager.cpp
   abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
   attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp
-  defeq_simplifier.cpp proof_irrel_expr_manager.cpp local_context.cpp metavar_context.cpp
-  type_context.cpp
-  # Legacy
-  justification.cpp constraint.cpp metavar.cpp
+  defeq_simplifier.cpp proof_irrel_expr_manager.cpp
+  local_context.cpp metavar_context.cpp type_context.cpp
+  # Legacy -- The following files will be eventually deleted
+  normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp
+  unifier.cpp match.cpp class_instance_resolution.cpp old_type_context.cpp
   legacy_type_context.cpp old_type_checker.cpp old_converter.cpp old_default_converter.cpp
-  old_util.cpp
+  old_util.cpp let.cpp metavar_closure.cpp old_local_context.cpp choice_iterator.cpp
+  tmp_type_context.cpp
   )