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

fix(kernel/justification): missing 'const'

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-26 08:18:18 -07:00
parent 52ff29a6f7
commit cdc41244ae
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/justification.cpp
View file

@ -194,7 +194,7 @@ optional<expr> justification::get_main_expr() const {
}
}
}
format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) {
format justification::pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) const {
justification_cell * it = m_ptr;
while (true) {
if (!it)

2
src/kernel/justification.h
View file

@ -61,7 +61,7 @@ public:
\brief Convert this justification into a format object. This method is usually used to report
"error" messages to users.
*/
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s);
format pp(formatter const & fmt, options const & opts, pos_info_provider const * p, substitution const & s) const;
/**
\brief Return an expression associated with the justification object.
*/