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

fix(frontends/lean/server): disable cache, when a definition is reused from the cache, we loose type information, fixes #35

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-12 17:35:32 -07:00
parent 2869d9059f
commit 2f48552f06
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/server.cpp
View file

@ -117,7 +117,7 @@ void server::process_from(unsigned linenum) {
m_ios.set_options(s.m_options);
parser p(s.m_env, m_ios, strm, m_file->m_fname.c_str(), false, 1, s.m_lds, s.m_eds, s.m_line,
&m_file->m_snapshots, &m_file->m_info);
p.set_cache(&m_cache);
// p.set_cache(&m_cache);
p();
}