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

fix(library/tactic/tactic_state): do not allocate tactic_state_cell using the VM allocator

Browse source
This commit is contained in:
Gabriel Ebner 2016-11-30 14:13:18 -05:00
parent 4df0f82934
commit e070444bbf
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tactic/tactic_state.cpp
View file

@ -45,13 +45,12 @@ unsigned get_pp_instantiate_goal_mvars(options const & o) {
}
void tactic_state_cell::dealloc() {
this->~tactic_state_cell();
get_vm_allocator().deallocate(sizeof(tactic_state_cell), this);
delete this;
}
tactic_state::tactic_state(environment const & env, options const & o, metavar_context const & ctx,
list<expr> const & gs, expr const & main) {
m_ptr = new (get_vm_allocator().allocate(sizeof(tactic_state_cell))) tactic_state_cell(env, o, ctx, gs, main);
m_ptr = new tactic_state_cell(env, o, ctx, gs, main);
m_ptr->inc_ref();
}