]> matita.cs.unibo.it Git - helm.git/commit
EXPERIMENTAL COMMIT (by CSC,actuall :-)
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 16:22:18 +0000 (16:22 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 16:22:18 +0000 (16:22 +0000)
commit5c8de084e314e41f3dc2f605f6242283e930b803
tree5b822131f07a9f2a16aa019edaa366b3d5cc6d29
parentc353df2f92c619afcbfcdf978df146239ed2db1c
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!
21 files changed:
helm/software/components/binaries/transcript/.depend.opt
helm/software/components/grafite_engine/grafiteEngine.ml
helm/software/components/grafite_engine/grafiteSync.ml
helm/software/components/grafite_engine/grafiteTypes.ml
helm/software/components/grafite_engine/grafiteTypes.mli
helm/software/components/ng_kernel/nCicLibrary.ml
helm/software/components/ng_kernel/nCicLibrary.mli
helm/software/components/ng_kernel/nUri.ml
helm/software/components/ng_kernel/nUri.mli
helm/software/components/ng_refiner/.depend
helm/software/components/ng_refiner/check.ml
helm/software/components/ng_refiner/nCicUnifHint.ml
helm/software/components/ng_refiner/nCicUnifHint.mli
helm/software/components/ng_refiner/nRstatus.ml
helm/software/components/ng_refiner/nRstatus.mli
helm/software/matita/matitaGui.ml
helm/software/matita/matitaWiki.ml
helm/software/matita/matitacLib.ml
helm/software/matita/tests/depends
helm/software/matita/tests/ng_include.ma [new file with mode: 0644]
helm/software/matita/tests/ng_includeB.ma [new file with mode: 0644]