max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(kernel/local_ctx): typo

Browse source
This commit is contained in:
Leonardo de Moura 2018-09-11 17:37:55 -07:00
parent 9b21287a3e
commit d814ee612a
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/kernel/local_ctx.cpp
View file

@ -81,7 +81,7 @@ local_decl const & local_ctx::get_local_decl(name const & n) const {
if (local_decl const * r = m_name2local_decl.find(n))
return *r;
else
throw exception(sstream() << "unknown local constant: " << n);
throw exception(sstream() << "unknown free variable: " << n);
}
expr local_ctx::get_local(name const & n) const {