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

chore(kernel/justification): fix compilation warning

Browse source
This commit is contained in:
Leonardo de Moura 2015-05-21 10:13:44 -07:00
parent 76e7f2e7d8
commit 6a87239a5d
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/kernel/justification.cpp
View file

@ -315,6 +315,7 @@ format justification::pp_core(formatter const & fmt, pos_info_provider const * p
format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false); format r2 = to_composite(it)->m_child[1].pp_core(fmt, p, s, set, false);
return r1 + r2; return r1 + r2;
}} }}
lean_unreachable();
} }
format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const { format justification::pp(formatter const & fmt, pos_info_provider const * p, substitution const & s) const {