From bfe64a703149c79c0b97bcbe6854c40032d19cbe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Feb 2014 21:30:26 -0800 Subject: [PATCH] fix(library/elaborator): hack for fixing a bug due to pairs/projs, this is temporary fix until we build a new elaborator Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index a37bf8ae5..540eaf450 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1389,7 +1389,7 @@ class elaborator::imp { } else if (is_abstraction(b)) { imitate_abstraction(a, b, c); return true; - } else if (is_app(b) && !has_metavar(arg(b, 0))) { + } else if (is_app(b) && (is_var(arg(b, 0)) || is_constant(arg(b, 0)) || is_value(arg(b, 0)))) { imitate_application(a, b, c); return true; } else if (is_proj(b)) {