From 0cf226220c9068fa9b6d413764401250e40ffa42 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Feb 2020 18:26:12 -0800 Subject: [PATCH] fix: remove incorrect assertion Note that `get_cases_on_minors_range` is now parametric on `m_before_erasure`: `get_cases_on_minors_range(env(), const_name(fn), m_before_erasure)` --- src/library/compiler/csimp.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index b688bf6319..71b86c0434 100644 --- a/src/library/compiler/csimp.cpp +++ b/src/library/compiler/csimp.cpp @@ -330,7 +330,6 @@ class csimp_fn { }; void collect_cases_info(expr e, cases_info_result & result) { - lean_assert(m_before_erasure); while (true) { if (is_lambda(e)) e = binding_body(e);