Instead of serializing closures (of type status -> status), we now
serialize data. This is achieved by implementing an existential type
NCicLibrary.Serializer(struct type status end).obj
whose semantics is "\exists 'a. 'a -> status -> status"
and by putting in the dump a list of these existential types.
The current implementation is the type-unsafe one based internally on Obj.magic.
However, the interface is (should be?) type-safe.
Other type-safe implementations could be derived by the ocaml m.l. thread on
existential types. In particular, I remember implementations via:
- references
- functors
- exceptions
- impredicative encoding via polymorphic methods
This fix allow to change the Matita code without invalidating the library.
(Critical) things still to be done:
- decompilation
- refreshment of URIs