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

fix(library/util): compilation error in debug mode

Browse source
This commit is contained in:
Leonardo de Moura 2015-06-03 17:39:03 -07:00
parent 68688ecdf6
commit c8ad1874a2
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/library/util.cpp
View file

@ -782,7 +782,7 @@ format format_goal(formatter const & fmt, buffer<expr> const & hyps, expr const
expr l = hyps[i];
format ids = fmt(l);
expr t = tmp_subst.instantiate(mlocal_type(l));
lean_assert(tmp.size() > 0);
lean_assert(hyps.size() > 0);
while (i < hyps.size() - 1) {
expr l2 = hyps[i+1];
expr t2 = tmp_subst.instantiate(mlocal_type(l2));