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

fix: mark a few more things as persistent

Browse source
This commit is contained in:
Sebastian Ullrich 2020-10-10 12:35:07 +02:00
parent c3c037b4de
commit f5565d1d92
2 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/kernel/declaration.cpp
View file

@ -312,7 +312,9 @@ bool constant_info::is_unsafe() const {
void initialize_declaration() {
g_opaque = new reducibility_hints(reducibility_hints::mk_opaque());
mark_persistent(g_opaque->raw());
g_dummy = new declaration(mk_axiom(name(), names(), expr()));
mark_persistent(g_dummy->raw());
}
void finalize_declaration() {

1
src/kernel/local_ctx.cpp
View file

@ -130,6 +130,7 @@ void initialize_local_ctx() {
g_dummy_decl = new local_decl(std::numeric_limits<unsigned>::max(),
name("__local_decl_for_default_constructor"), name("__local_decl_for_default_constructor"),
mk_Prop(), mk_binder_info());
mark_persistent(g_dummy_decl->raw());
}
void finalize_local_ctx() {