fix(frontends/lean/elaborator): compilation problem

This commit is contained in:
Leonardo de Moura 2015-01-11 20:58:41 -08:00
parent 08a7997a97
commit 4f519be55e

View file

@ -1506,7 +1506,6 @@ void elaborator::display_unassigned_mvars(expr const & e, substitution const & s
proof_state ps(goals(g), s, m_ngen, constraints(), relax);
display_unsolved_proof_state(mvar, ps, "don't know how to synthesize placeholder");
}
return false;
});
}
}