From 88a62f9f7e832b718d6c71917fbc0ca1a188b04b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 6 Mar 2020 12:12:23 -0800 Subject: [PATCH] fix: #121 in the old frontend This is temporary hack. We will delete this module in the near future. --- src/library/type_context.cpp | 12 ++++++++++-- tests/lean/run/121.lean | 2 +- 2 files changed, 11 insertions(+), 3 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 3f91467b90..d6b72d9df1 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -1918,8 +1918,16 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) { use_fo = true; } - if (use_fo && (is_app(new_v) || !m_unifier_cfg.m_const_approx)) { - return process_assignment_fo_approx(mvar, args, new_v); + if (use_fo) { + if (is_app(new_v) || !m_unifier_cfg.m_const_approx) { + return process_assignment_fo_approx(mvar, args, new_v); + } else { + scope s(*this); + if (process_assignment_fo_approx(mvar, args, new_v)) { + s.commit(); + return true; + } + } } if (optional new_new_v = check_assignment(locals, in_ctx_locals, mvar, new_v)) diff --git a/tests/lean/run/121.lean b/tests/lean/run/121.lean index 893e3cf31d..c85508e08b 100644 --- a/tests/lean/run/121.lean +++ b/tests/lean/run/121.lean @@ -2,7 +2,7 @@ abbrev DelabM := Id abbrev Delab := DelabM Nat example : DelabM Nat := pure 1 -- works --- example : Delab := pure 1 -- fails in old frontend +example : Delab := pure 1 -- works new_frontend