From 1e40525a0c2d78c72c0233d3e3e404e079c379ac Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Jul 2014 21:15:32 -0700 Subject: [PATCH] fix(library/unifier): simple bug Signed-off-by: Leonardo de Moura --- src/library/unifier.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 0c8f2fbda..69bcb5530 100644 --- a/src/library/unifier.cpp +++ b/src/library/unifier.cpp @@ -1055,8 +1055,7 @@ struct unifier_fn { Given, m := a metavariable ?m margs := [a_1 ... a_k] - We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple projections" IF - rhs is NOT an application. + We say a unification problem (?m a_1 ... a_k) =?= rhs uses "simple projections" when If (rhs and a_i are *not* local constants) OR (rhs is a local constant and a_i is a metavariable application), then we add the constraints @@ -1073,7 +1072,6 @@ struct unifier_fn { buffer & alts) { lean_assert(is_metavar(m)); lean_assert(!is_meta(rhs)); - lean_assert(!is_app(rhs)); expr const & mtype = mlocal_type(m); unsigned i = margs.size(); while (i > 0) { @@ -1133,6 +1131,7 @@ struct unifier_fn { alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, mk_var(vidx), rhs, j)); } } else if (is_constant(f)) { + add_simple_projections(m, margs, rhs, j, alts); alts.push_back(mk_flex_rigid_app_cnstrs(m, margs, f, rhs, j)); } else { lean_unreachable(); // LCOV_EXCL_LINE