From 33fe409dc66120e9318f8f06f850775e9b4b64b3 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 27 Sep 2014 22:24:36 -0700 Subject: [PATCH] chore(frontends/lean/placeholder_elaborator): cleanup --- src/frontends/lean/placeholder_elaborator.cpp | 10 ---------- 1 file changed, 10 deletions(-) diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 7dfdc3669..40ee9f333 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -268,16 +268,6 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const justification j = mk_failed_to_synthesize_jst(env, m); auto choice_fn = [=](expr const & meta, expr const & meta_type, substitution const & s, name_generator const & ngen) { - if (has_expr_metavar_relaxed(meta_type)) { - // TODO(Leo): remove - if (factor.on_demand()) { - constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, to_delay_factor(cnstr_group::Basic)); - return lazy_list(constraints(delayed_c)); - } else if (factor.explict_value() < to_delay_factor(cnstr_group::ClassInstance)) { - constraint delayed_c = mk_placeholder_root_cnstr(C, m, is_strict, cfg, factor.explict_value()+1); - return lazy_list(constraints(delayed_c)); - } - } if (!is_ext_class(C->tc(), meta_type)) { // do nothing, since type is not a class. return lazy_list(constraints());