Procedural: we corrected two errors about the handling of mutcase (the "cases"

[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 c1b23c9281697c18c3ac5d6ad8c0b5431fc0abf9..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
@@ -115,13 +116,14 @@ let time_travel ~present ~past =
   CoercDb.restore past.GrafiteTypes.coercions;
 ;;
 
-let initial_status baseuri = {
+let initial_status lexicon_status baseuri = {
     GrafiteTypes.moo_content_rev = [];
     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;
   }