]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteSync.ml
EXPERIMENTAL COMMIT (by CSC,actuall :-)
[helm.git] / helm / software / components / grafite_engine / grafiteSync.ml
index a773ea401a9361a88cf982402bf58af8ae7bec46..60bfc69217b71425f922440ec50c69a0bba50637 100644 (file)
@@ -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;
       };
   }
 }