]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5c8de08) | patch
EXPERIMENTAL COMMIT (part B, by CSC :-):
authorEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 16:41:47 +0000 (16:41 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Mon, 15 Jun 2009 16:41:47 +0000 (16:41 +0000)
commit62a12215bbf8686fab44e8db25babd3095983c8f
tree66cb882025a78c57cc8283f2f9bd39b93eef14datree | snapshot
parent5c8de084e314e41f3dc2f605f6242283e930b803commit | diff
EXPERIMENTAL COMMIT (part B, by CSC :-):
 - objects are now individually serialized too
   (but never decompiled)

CRITICAL OBSERVATION:
 - closures in ocaml are pointers in the binary, hence the library
   must be decompiled at every single change in matita's code
helm/software/components/ng_kernel/nCicLibrary.ml diff | blob | history
helm/software/matita/tests/ng_include.ma diff | blob | history
helm/software/matita/tests/ng_includeB.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.