X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=60bfc69217b71425f922440ec50c69a0bba50637;hb=5c8de084e314e41f3dc2f605f6242283e930b803;hp=a773ea401a9361a88cf982402bf58af8ae7bec46;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml index a773ea401..60bfc6921 100644 --- a/helm/software/components/grafite_engine/grafiteSync.ml +++ b/helm/software/components/grafite_engine/grafiteSync.ml @@ -171,6 +171,7 @@ let time_travel ~present ~past = uri_list_diff present.GrafiteTypes.objects past.GrafiteTypes.objects in List.iter LibrarySync.remove_obj objs_to_remove; CoercDb.restore past.GrafiteTypes.coercions; + NCicLibrary.time_travel (GrafiteTypes.get_library_db past) ;; let initial_status lexicon_status baseuri = { @@ -185,6 +186,8 @@ let initial_status lexicon_status baseuri = { NEstatus.rstatus = { NRstatus.uhint_db = NCicUnifHint.empty_db; NRstatus.coerc_db = NCicCoercion.empty_db; + NRstatus.library_db = NCicLibrary.time0; + NRstatus.dump = fun x -> x; }; } }