Extracted code for the whole compiler. The space cost model is not there yet.
I have fixed by hand the few extraction problems (i.e. composed coercions not extracted and type definitions with wrong syntax).
I have also changed all axioms to be implemented so that they do not fail at initialization time.