X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=74e2cf2e26ed75042b6c13125448839b35b23a0b;hb=df1201e37d6f2631dc31ffc87b979a6c81180a3a;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..74e2cf2e2 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -147,12 +147,11 @@ let add_coercion ~pack_coercion_obj ~add_composites status uri arity
    objects = lemmas @ status.GrafiteTypes.objects;
   }
  in
- let db = 
-   NCicCoercion.index_old_db (CoercDb.dump ()) 
-    (GrafiteTypes.get_coercions status) 
+ let estatus =
+  NCicCoercion.index_old_db (CoercDb.dump ()) (GrafiteTypes.get_estatus status)
  in
- let status = GrafiteTypes.set_coercions db status in 
- status, lemmas
+ let status = GrafiteTypes.set_estatus estatus status in
+  status, lemmas
 
 let prefer_coercion s u = 
   CoercDb.prefer u;
@@ -171,6 +170,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_estatus past)
 ;;
 
 let initial_status lexicon_status baseuri = {
@@ -180,13 +180,7 @@ let initial_status lexicon_status baseuri = {
     coercions = CoercDb.empty_coerc_db;
     automation_cache = AutomationCache.empty ();
     baseuri = baseuri;
-    ng_status = GrafiteTypes.CommandMode { 
-      NEstatus.lstatus = lexicon_status;
-      NEstatus.rstatus = {
-        NRstatus.uhint_db = NCicUnifHint.empty_db;
-        NRstatus.coerc_db = NCicCoercion.empty_db;
-      };
-  }
+    ng_status = GrafiteTypes.CommandMode (new NEstatus.status)
 }