From d4541ce2cc16fece6559629ee2f4b210577f2948 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Mon, 6 Feb 2017 20:44:28 +0100 Subject: [PATCH] chore(frontends/lean/elaborator): fix clang-3.4 build error --- src/frontends/lean/elaborator.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 6438f6d3f7..0e7d38aaf1 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -2725,7 +2725,7 @@ expr elaborator::visit(expr const & e, optional const & expected_type) { flet inc_depth(m_depth, m_depth+1); trace_elab_detail(tout() << "[" << m_depth << "] visiting\n" << e << "\n"; if (expected_type) tout() << "expected type:\n" << instantiate_mvars(*expected_type) << "\n";); - return recover_expr_from_exception(expected_type, e, [&] { + return recover_expr_from_exception(expected_type, e, [&] () -> expr { if (is_placeholder(e)) { return visit_placeholder(e, expected_type); } else if (is_have_expr(e)) {