From 2aa691ccb350d992fe276049485745f1b34909db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Dec 2013 21:11:25 -0800 Subject: [PATCH] fix(kernel/replace_fn): ignore the cached type in constants Signed-off-by: Leonardo de Moura --- src/kernel/replace_fn.h | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h index 62df67c964..e9cff162ca 100644 --- a/src/kernel/replace_fn.h +++ b/src/kernel/replace_fn.h @@ -62,9 +62,8 @@ class replace_fn { static bool is_atomic(expr const & e) { switch (e.kind()) { - case expr_kind::Constant: - return !const_type(e); - case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: + case expr_kind::Var: case expr_kind::MetaVar: return true; default: return false; @@ -143,14 +142,8 @@ public: expr const & e = f.m_expr; unsigned offset = f.m_offset; switch (e.kind()) { - case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: + case expr_kind::Constant: case expr_kind::Type: case expr_kind::Value: case expr_kind::Var: case expr_kind::MetaVar: lean_unreachable(); // LCOV_EXCL_LINE - case expr_kind::Constant: - if (check_index(f, 0) && !visit(*const_type(e), offset)) - goto begin_loop; - r = update_const(e, some_expr(rs(-1))); - pop_rs(1); - break; case expr_kind::App: { unsigned num = num_args(e); while (f.m_index < num) {