Universe is used only locally to tactics/

[helm.git] / helm / software / components / grafite_engine / grafiteSync.ml

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index 5a746f41c8ee727e9346bc7daec2eaaee61f63e0..999d961369324bd1c3be5df1661e244982cce0f1 100644 (file)
--- 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;
   }