From 38a25a1bd212256769dbff03c4dc42285c86dbe6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Dec 2013 09:27:25 -0800 Subject: [PATCH] feat(kernel/metavar): (re-)enable add_lift simplification Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 3f2a6af57..510d08c02 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -319,9 +319,6 @@ bool has_assigned_metavar(expr const & e, metavar_env const & menv) { local_context add_lift(local_context const & lctx, unsigned s, unsigned n) { if (n == 0) return lctx; -#if 0 - // Remark: I disabled the following simplification. - // It impacts negatively the heuristics used in the elaborator. if (lctx) { local_entry e = head(lctx); // Simplification rule @@ -330,7 +327,6 @@ local_context add_lift(local_context const & lctx, unsigned s, unsigned n) { return add_lift(tail(lctx), e.s(), e.n() + n); } } -#endif return cons(mk_lift(s, n), lctx); }