From 7b2fea3fabea456508302ebe956bd69ae25462f1 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Dec 2013 08:46:36 -0800 Subject: [PATCH] fix(kernel/normalizer): compilation problem with clang++ Signed-off-by: Leonardo de Moura --- src/kernel/normalizer.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp index d5ccf042a1..abffc17523 100644 --- a/src/kernel/normalizer.cpp +++ b/src/kernel/normalizer.cpp @@ -117,7 +117,7 @@ class normalizer::imp { /** \brief Convert the value \c v back into an expression in a context that contains \c k binders. */ expr reify(expr const & v, unsigned k) { - return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) { + return replace(v, [&](expr const & e, unsigned DEBUG_CODE(offset)) -> expr { lean_assert(offset == 0); lean_assert(!is_lambda(e) && !is_pi(e) && !is_metavar(e) && !is_let(e)); if (is_var(e)) {