michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/placeholder_elaborator): missing 'return'

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-25 15:00:06 -07:00
parent 03f71c73dc
commit bcb30f6232
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/frontends/lean/placeholder_elaborator.cpp
View file

@ -279,7 +279,7 @@ constraint mk_placeholder_root_cnstr(std::shared_ptr<placeholder_context> const
return map2<constraints>(seq, [=](pair<substitution, constraints> 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