From e070444bbfbee790448f05825fa07de8e9515aca Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Wed, 30 Nov 2016 14:13:18 -0500 Subject: [PATCH] fix(library/tactic/tactic_state): do not allocate tactic_state_cell using the VM allocator --- src/library/tactic/tactic_state.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp index 1c507ba938..69b1984941 100644 --- a/src/library/tactic/tactic_state.cpp +++ b/src/library/tactic/tactic_state.cpp @@ -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 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(); }