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

fix(library/norm_num): memory leaks

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-19 14:32:47 -08:00
parent ee3083c12c
commit 86ad8c348e
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/library/norm_num.cpp
View file

@ -1198,5 +1198,11 @@ void finalize_norm_num() {
delete g_mul_div;
delete g_nonzero_div;
delete g_neg_zero;
delete g_lin_ord_ring;
delete g_lin_ord_semiring;
delete g_field;
delete g_nonzero_neg;
delete g_subst_div;
delete g_nonzero_pos;
}
}