diff --git a/src/library/compiler/closed_term_cache.cpp b/src/library/compiler/closed_term_cache.cpp index a7cbb5f8e8..0faca833d6 100644 --- a/src/library/compiler/closed_term_cache.cpp +++ b/src/library/compiler/closed_term_cache.cpp @@ -56,7 +56,7 @@ struct ct_cache_modification : public modification { }; optional get_closed_term_name(environment const & env, expr const & e) { - lean_assert(!has_fvars(e)); + lean_assert(!has_fvar(e)); lean_assert(!has_loose_bvars(e)); closed_term_ext const & ext = get_extension(env); if (name const * c = ext.m_cache.find(e)) { diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index 62fc58978b..42f5b5216e 100644 --- a/src/library/compiler/llnf.cpp +++ b/src/library/compiler/llnf.cpp @@ -1238,7 +1238,6 @@ class explicit_boxing_fn { lean_assert(is_constant(f)); name const & fn = const_name(f); if (is_cases_on_recursor(env(), fn)) { - lean_assert(!is_let_val); return visit_cases(f, args); } else if (is_llnf_closure(f)) { return visit_closure(f, args);