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

fix(frontends/lean): add hack for flycheck

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-01 16:26:04 -07:00
parent 288831dc66
commit 4b604521a0
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/frontends/lean/elaborator.cpp
View file

@ -1257,7 +1257,7 @@ public:
if (!prev || p.first != prev->first) { if (!prev || p.first != prev->first) {
auto out = regular(m_env, m_ios); auto out = regular(m_env, m_ios);
flyinfo_scope info(out); flyinfo_scope info(out);
out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second out << m_pos_provider->get_file_name() << ":" << p.first.first << ":" << p.first.second+1
<< ": type\n" << p.second << endl; << ": type\n" << p.second << endl;
prev = p; prev = p;
} }