From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 15 Jun 2009 16:22:18 +0000 (+0000)
Subject: EXPERIMENTAL COMMIT (by CSC,actuall :-)
X-Git-Tag: make_still_working~3868
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=5c8de084e314e41f3dc2f605f6242283e930b803;hp=5c8de084e314e41f3dc2f605f6242283e930b803;p=helm.git

EXPERIMENTAL COMMIT (by CSC,actuall :-)
This commit partially implements (in NCicLibrary) serialization for NG.
It creates several .matita/matita/.../foo.ng files that are ocaml dumps
of closures (NRstatus.refiner_status -> NRstatus.refiner_status) to be applied
to the current status.

The test tests/ng_includeB.ma shows how unification hints are preserved.

TODO:
 a) decompilation is implemented in NCicLibrary, but not called anywhere
 b) serialization of objects (and "query" db (and old to new cache??)) not
    implemented yet
 c) objects are removed from the library, but not from the environment!
---