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

fix(library/scoped_ext): typo in error message

Browse source
This commit is contained in:
Scott Morrison 2017-01-13 20:51:03 +11:00 • committed by Leonardo de Moura
parent 69fd35f068
commit 6f8fc0fe06
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/scoped_ext.cpp
View file

@ -173,7 +173,7 @@ environment pop_scope(environment const & env, io_state const & ios, name const
if (is_nil(ext.m_namespaces))
throw exception("invalid end of scope, there are no open namespaces/sections");
if (n != head(ext.m_headers))
throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
throw exception(sstream() << "invalid end of scope, begin/end mismatch, scope starts with '"
<< head(ext.m_headers) << "', and ends with '" << n << "'");
return pop_scope_core(env, ios);
}