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 to_goal(environment const & env, context const & buffer> hypotheses; // normalized names and types of the entries processed so far buffer bodies; // normalized bodies of the entries processed so far std::vector 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) {