diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 2753121df9..230dc7ba7b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -69,6 +69,7 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET(type_context_cache_manager, get_tcm, true /* use binder information at infer_cache */);
 
 static name * g_elab_strategy = nullptr;
diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index 30b1cddfb6..5a389fbfd9 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -95,6 +95,7 @@ public:
     }
 };
 
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET_DEF(mk_binding_cache, get_mk_binding_cache);
 
 template<bool is_lambda>
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index deb8947467..9e6f593e1f 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -406,6 +406,7 @@ expr_macro::~expr_macro() {}
 // Constructors
 LEAN_THREAD_VALUE(bool, g_expr_cache_enabled, false);
 typedef typename std::unordered_set<expr, expr_hash, is_bi_equal_proc> expr_cache;
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET_DEF(expr_cache, get_expr_cache);
 
 struct cache_expr_insert_fn {
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 6d3ba8426c..e50887d168 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -49,6 +49,7 @@ struct eq_cache {
     }
 };
 
+/* CACHE_RESET: No */
 MK_THREAD_LOCAL_GET_DEF(eq_cache, get_eq_cache);
 
 /** \brief Functional object for comparing expressions.
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index 320d3c7510..cc610e5178 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -48,6 +48,7 @@ struct for_each_cache {
     }
 };
 
+/* CACHE_RESET: NO */
 MK_CACHE_STACK(for_each_cache, LEAN_DEFAULT_FOR_EACH_CACHE_CAPACITY)
 
 class for_each_fn {
diff --git a/src/kernel/instantiate.cpp b/src/kernel/instantiate.cpp
index c38c1d0be8..58d6edd95d 100644
--- a/src/kernel/instantiate.cpp
+++ b/src/kernel/instantiate.cpp
@@ -189,6 +189,7 @@ expr instantiate_univ_params(expr const & e, level_param_names const & ps, level
         });
 }
 
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_type_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
 MK_THREAD_LOCAL_GET(instantiate_univ_cache, get_value_univ_cache, LEAN_INST_UNIV_CACHE_SIZE);
 
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 87e7cd7525..41e14c3b12 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -247,6 +247,7 @@ bool is_one(level const & l) { return l == mk_level_one(); }
 
 typedef typename std::unordered_set<level, level_hash> level_cache;
 LEAN_THREAD_VALUE(bool, g_level_cache_enabled, false);
+/* CACHE_RESET: No */
 MK_THREAD_LOCAL_GET_DEF(level_cache, get_level_cache);
 bool enable_level_caching(bool f) {
     bool r = g_level_cache_enabled;
diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index a6dc3bae41..9e366ddecf 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -52,6 +52,7 @@ struct replace_cache {
     }
 };
 
+/* CACHE_RESET: NO */
 MK_CACHE_STACK(replace_cache, LEAN_DEFAULT_REPLACE_CACHE_CAPACITY)
 
 class replace_rec_fn {
diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp
index bf2a788418..2a6b519213 100644
--- a/src/library/app_builder.cpp
+++ b/src/library/app_builder.cpp
@@ -123,6 +123,7 @@ public:
 
 typedef cache_compatibility_helper<app_builder_cache> app_builder_cache_helper;
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(app_builder_cache_helper, get_abch);
 
 /** Return an app_builder_cache for the transparency_mode in ctx, and compatible with the environment. */
diff --git a/src/library/congr_lemma.cpp b/src/library/congr_lemma.cpp
index 06f9887423..471a783ead 100644
--- a/src/library/congr_lemma.cpp
+++ b/src/library/congr_lemma.cpp
@@ -41,6 +41,7 @@ struct congr_lemma_cache {
 
 typedef cache_compatibility_helper<congr_lemma_cache> congr_lemma_cache_helper;
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(congr_lemma_cache_helper, get_clch);
 
 congr_lemma_cache & get_congr_lemma_cache_for(type_context const & ctx) {
diff --git a/src/library/fun_info.cpp b/src/library/fun_info.cpp
index 0b1da555c1..75b94e460e 100644
--- a/src/library/fun_info.cpp
+++ b/src/library/fun_info.cpp
@@ -53,6 +53,7 @@ struct fun_info_cache {
 
 typedef cache_compatibility_helper<fun_info_cache> fun_info_cache_helper;
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(fun_info_cache_helper, get_fich);
 
 fun_info_cache & get_fun_info_cache_for(type_context const & ctx) {
diff --git a/src/library/tactic/ac_tactics.cpp b/src/library/tactic/ac_tactics.cpp
index 5eff233f38..e8d86ef626 100644
--- a/src/library/tactic/ac_tactics.cpp
+++ b/src/library/tactic/ac_tactics.cpp
@@ -30,6 +30,7 @@ struct ac_manager_old::cache {
         m_instance_fingerprint(get_instance_fingerprint(env)) {}
 };
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(ac_manager_old::cache_ptr, get_cache_ptr);
 
 static ac_manager_old::cache_ptr get_cache(environment const & env) {
diff --git a/src/library/tactic/simp_lemmas.cpp b/src/library/tactic/simp_lemmas.cpp
index 1fae1ca31d..2cc3a6b463 100644
--- a/src/library/tactic/simp_lemmas.cpp
+++ b/src/library/tactic/simp_lemmas.cpp
@@ -1199,6 +1199,9 @@ public:
     }
 };
 
+/* CACHE_RESET: YES
+
+   Do we still need this cache? Can we use user_attr_cache infrastructure. */
 MK_THREAD_LOCAL_GET_DEF(simp_lemmas_cache, get_cache);
 
 simp_lemmas get_simp_lemmas(environment const & env, simp_lemmas_token tk) {
diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp
index 5ac11e389f..4e396f5f87 100644
--- a/src/library/tactic/smt/congruence_closure.cpp
+++ b/src/library/tactic/smt/congruence_closure.cpp
@@ -94,6 +94,7 @@ public:
     }
 };
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(ext_congr_lemma_cache_manager, get_clcm);
 
 congruence_closure::congruence_closure(type_context & ctx, state & s, defeq_canonizer::state & dcs,
diff --git a/src/library/tactic/smt/ematch.cpp b/src/library/tactic/smt/ematch.cpp
index 3318f36f7f..f74c5757ee 100644
--- a/src/library/tactic/smt/ematch.cpp
+++ b/src/library/tactic/smt/ematch.cpp
@@ -90,6 +90,7 @@ vm_obj ematch_state::mk_vm_ematch_config() const {
     return mk_vm_constructor(0, mk_vm_nat(get_config().m_max_instances), mk_vm_nat(get_config().m_max_generation));
 }
 
+/* CACHE_RESET: NO */
 /* Allocator for ematching constraints. */
 MK_THREAD_LOCAL_GET(small_object_allocator, get_emc_allocator, "ematch constraint");
 
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index c1df3edcf3..bd975ce811 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -321,6 +321,7 @@ vm_obj tactic_target(vm_obj const & o) {
     return tactic::mk_success(to_obj(g->get_type()), s);
 }
 
+/* CACHE_RESET: YES */
 MK_THREAD_LOCAL_GET_DEF(type_context_cache_manager, get_tcm);
 
 type_context mk_type_context_for(environment const & env, options const & o, metavar_context const & mctx,
diff --git a/src/library/tactic/user_attribute.cpp b/src/library/tactic/user_attribute.cpp
index 79f50f57de..de51233f92 100644
--- a/src/library/tactic/user_attribute.cpp
+++ b/src/library/tactic/user_attribute.cpp
@@ -232,6 +232,10 @@ struct user_attr_cache {
     name_hash_map<entry> m_cache;
 };
 
+/* CACHE_RESET: NO
+
+   This cache contains vm_objects.
+*/
 MK_THREAD_LOCAL_GET_DEF(user_attr_cache, get_user_attribute_cache);
 
 static bool check_dep_fingerprints(environment const & env, list<name> const & dep_names, list<unsigned> const & dep_fingerprints) {
diff --git a/src/library/type_context.h b/src/library/type_context.h
index 748045f09c..e711f186e8 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -41,7 +41,10 @@ bool is_at_least_instances(transparency_mode m);
 transparency_mode ensure_semireducible_mode(transparency_mode m);
 transparency_mode ensure_instances_mode(transparency_mode m);
 
-/* \brief Cached information for type_context. */
+/* \brief Cached information for type_context.
+
+   TODO(Leo): reevaluate the cache validation policies we use.
+ */
 class type_context_cache {
     typedef std::unordered_map<name, optional<declaration>, name_hash> transparency_cache;
     typedef std::unordered_map<name, bool, name_hash> name2bool;
diff --git a/src/util/fresh_name.cpp b/src/util/fresh_name.cpp
index 9a5cbbc9f7..ea5dd3eba7 100644
--- a/src/util/fresh_name.cpp
+++ b/src/util/fresh_name.cpp
@@ -20,7 +20,9 @@ static void register_fresh_name_prefix(name const & p) {
     g_fresh_name_prefixes->insert(p);
 }
 
+/* CACHE_RESET: NO */
 MK_THREAD_LOCAL_GET_DEF(name, get_prefix);
+/* CACHE_RESET: YES */
 LEAN_THREAD_VALUE(unsigned, g_next_idx, 0);
 
 static bool is_fresh_prefix(name const & p) {
@@ -37,6 +39,7 @@ name mk_fresh_name() {
         prefix = name::mk_internal_unique_name();
         register_fresh_name_prefix(prefix);
     }
+    /* REMARK: after we implement RESET operation we will not need the following test anymore */
     if (g_next_idx == std::numeric_limits<unsigned>::max()) {
         // avoid overflow
         prefix = name(prefix, g_next_idx);