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

fix(frontends/lean/parser): copy environment from snapshot

Browse source
This commit is contained in:
Gabriel Ebner 2016-10-13 10:59:25 -04:00 • committed by Leonardo de Moura
parent 5c76489921
commit 73b685db2e
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/frontends/lean/parser.cpp
View file

@ -197,6 +197,7 @@ parser::parser(environment const & env, io_state const & ios,
m_in_pattern = false;
m_has_params = false;
if (s) {
m_env = s->m_env;
m_messages = s->m_messages;
m_local_level_decls = s->m_lds;
m_local_decls = s->m_eds;