From 309e7ba8806ea72e7c1790c10fbc7980a1ee860d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 24 Feb 2014 15:26:21 -0800 Subject: [PATCH] fix(library/elaborator): temporary fix for bug reported by Jeremy Signed-off-by: Leonardo de Moura --- src/library/elaborator/elaborator.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/library/elaborator/elaborator.cpp b/src/library/elaborator/elaborator.cpp index 540eaf450..edad07735 100644 --- a/src/library/elaborator/elaborator.cpp +++ b/src/library/elaborator/elaborator.cpp @@ -1727,6 +1727,11 @@ class elaborator::imp { if (!eq && is_bool(a) && is_type(b)) return true; + if ((is_proj(a) && instantiate_metavars(true, a, c)) || + (is_proj(b) && instantiate_metavars(false, b, c))) { + return true; + } + if (a.kind() == b.kind()) { switch (a.kind()) { case expr_kind::Constant: case expr_kind::Var: case expr_kind::Value: