]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_engine/grafiteSync.ml
we rebuilt the dependences
[helm.git] / helm / software / components / grafite_engine / grafiteSync.ml
index 3fc67f2fda4f71b9dde3ddfa08c99e7b4f4e0122..5a746f41c8ee727e9346bc7daec2eaaee61f63e0 100644 (file)
@@ -115,14 +115,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;
     baseuri = baseuri;
-    ng_status = None;
+    ng_status = GrafiteTypes.CommandMode lexicon_status;
   }