X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=999d961369324bd1c3be5df1661e244982cce0f1;hb=b4f6b1a39b59e923527f5c17d8fdd0fa1e13e1bf;hp=5a746f41c8ee727e9346bc7daec2eaaee61f63e0;hpb=ec0b4acecb86886baf5f785da270fd60e7910b32;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 5a746f41c..999d96136 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -77,12 +77,13 @@ let add_obj ~pack_coercion_obj uri obj status =
  in
  let universe,status =
    List.fold_left add_to_universe 
-     (status.GrafiteTypes.universe,status) 
+     (status.GrafiteTypes.automation_cache.AutomationCache.univ,status) 
      uris_to_index 
  in
+ let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in
   {status with 
      GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
-     GrafiteTypes.universe = universe},
+     GrafiteTypes.automation_cache = cache },
    lemmas
 
 let add_coercion ~pack_coercion_obj ~add_composites status uri arity
@@ -120,7 +121,7 @@ let initial_status lexicon_status baseuri = {
     proof_status = GrafiteTypes.No_proof;
     objects = [];
     coercions = CoercDb.empty_coerc_db;
-    universe = Universe.empty;
+    automation_cache = AutomationCache.empty;
     baseuri = baseuri;
     ng_status = GrafiteTypes.CommandMode lexicon_status;
   }