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

fix(frontends/lean/decl_cmds): do not save 'examples' in .ilean file

Browse source
This commit is contained in:
Leonardo de Moura 2014-11-03 16:13:46 -08:00
parent 7afa69577e
commit 922e66c42f
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/decl_cmds.cpp
View file

@ -486,7 +486,7 @@ static environment definition_cmd_core(parser & p, def_cmd_kind kind, bool is_op
env = module::add(env, check(env, mk_definition(env, real_n, new_ls, type, value, is_opaque)));
p.cache_definition(real_n, pre_type, pre_value, new_ls, type, value);
}
if (!is_private)
if (!is_private && kind != Example)
p.add_decl_index(real_n, n_pos, p.get_cmd_token(), type);
}