diff --git a/src/frontends/lean/placeholder_elaborator.cpp b/src/frontends/lean/placeholder_elaborator.cpp index 0ee8a7f486..38233cca99 100644 --- a/src/frontends/lean/placeholder_elaborator.cpp +++ b/src/frontends/lean/placeholder_elaborator.cpp @@ -279,7 +279,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr const return map2(seq, [=](pair const & p) { substitution new_s = p.first; if (!new_s.is_expr_assigned(mlocal_name(get_app_fn(new_meta)))) - constraints(); + return constraints(); constraints postponed = map(p.second, [&](constraint const & c) { // we erase internal justifications