From 367108edfa4bbbd15adc6e0c2801e75edd75fb56 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Nov 2013 08:53:37 -0800
Subject: [PATCH] fix(library/tactic): compilation problem reported by clang++

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/tactic/goal.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/tactic/goal.cpp b/src/library/tactic/goal.cpp
index 02691d43ed..bfbc32044c 100644
--- a/src/library/tactic/goal.cpp
+++ b/src/library/tactic/goal.cpp
@@ -65,7 +65,7 @@ std::pair<goal, goal_proof_fn> to_goal(environment const & env, context const &
     buffer<std::pair<name, expr>> hypotheses;  // normalized names and types of the entries processed so far
     buffer<expr> bodies;                       // normalized bodies of the entries processed so far
     std::vector<expr> consts;                  // cached consts[i] == mk_constant(names[i], hypotheses[i])
-    auto replace_vars = [&](expr const & e, unsigned offset) {
+    auto replace_vars = [&](expr const & e, unsigned offset) -> expr {
         if (is_var(e)) {
             unsigned vidx = var_idx(e);
             if (vidx >= offset) {