From dce1de3905e798e40c77d9edd409057a2a70917c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 8 Nov 2019 10:03:02 -0800 Subject: [PATCH] chore: remove `transparency_mode::None` --- src/frontends/lean/elaborator.cpp | 2 +- src/library/abstract_context_cache.cpp | 2 -- src/library/abstract_context_cache.h | 4 ++-- src/library/type_context.cpp | 3 --- 4 files changed, 3 insertions(+), 8 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index f2972bdcd6..3d584401f5 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2267,7 +2267,7 @@ class validate_and_collect_lhs_mvars : public replace_visitor { of definitions compiled using the equation compiler */ { /* Try without use delta reduction */ - type_context_old::transparency_scope scope(ctx(), transparency_mode::None); + type_context_old::transparency_scope scope(ctx(), transparency_mode::Reducible); // it was None expr new_e = ctx().whnf(e); if (new_e != e) return some_expr(new_e); } diff --git a/src/library/abstract_context_cache.cpp b/src/library/abstract_context_cache.cpp index f2398a42ba..bfb5874eb9 100644 --- a/src/library/abstract_context_cache.cpp +++ b/src/library/abstract_context_cache.cpp @@ -73,8 +73,6 @@ context_cacheless::context_cacheless(abstract_context_cache const & c, bool): } bool context_cacheless::is_transparent(type_context_old & ctx, transparency_mode m, constant_info const & info) { - if (m == transparency_mode::None) - return false; name const & n = info.get_name(); if (get_proj_info(ctx, n)) return false; diff --git a/src/library/abstract_context_cache.h b/src/library/abstract_context_cache.h index 1de2c4c31e..6817fd455a 100644 --- a/src/library/abstract_context_cache.h +++ b/src/library/abstract_context_cache.h @@ -12,8 +12,8 @@ Author: Leonardo de Moura #include "library/fun_info.h" namespace lean { -#define LEAN_NUM_TRANSPARENCY_MODES 5 -enum class transparency_mode { All = 0, Semireducible, Reducible, None }; +#define LEAN_NUM_TRANSPARENCY_MODES 3 +enum class transparency_mode { All = 0, Semireducible, Reducible }; class type_context_old; diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 71d65a30c3..b6ec198c78 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -2995,9 +2995,6 @@ lbool type_context_old::try_numeral_eq_numeral(expr const & t, expr const & s) { /* Solve offset constraints. See discussion at issue #1226 */ lbool type_context_old::try_nat_offset_cnstrs(expr const & t, expr const & s) { - /* We should not use this feature when transparency_mode is none. - See issue #1295 */ - if (m_transparency_mode == transparency_mode::None) return l_undef; lbool r; r = try_offset_eq_offset(t, s); if (r != l_undef) return r;