Ensure that the memory pool can be reused after a rewind and get rid of the segmented array.

This commit is contained in:
Roberto Raggi
2010-03-18 15:21:07 +01:00
parent 1e2af0a77d
commit 61a504c427
17 changed files with 132 additions and 262 deletions

View File

@@ -53,7 +53,6 @@
#include "CoreTypes.h"
#include "Symbols.h"
#include "Names.h"
#include "Array.h"
#include "TypeMatcher.h"
#include <map>
#include <set>