=========================
EXTRACTION BUGS:
=========================

New bug: some function has type "__ foo" in the .ml and "'a foo" in the .mli.
The latter is incorrect.

=========================
AXIOMS TO BE IMPLEMENTED:
=========================

In order to plug the untrusted code, the following files needs manual
intervention:

a) compiler.ml: the two failwith must be replaced with calls to the
   untrusted code
b) the build script removed set_adt to favour the untrusted implementation