FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:

[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 60bfc69217b71425f922440ec50c69a0bba50637..de578d7ca6fd8365296dce1eb6033744687d443f 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -184,10 +184,11 @@ let initial_status lexicon_status baseuri = {
     ng_status = GrafiteTypes.CommandMode { 
       NEstatus.lstatus = lexicon_status;
       NEstatus.rstatus = {
+       NRstatus.refiner_status = {
         NRstatus.uhint_db = NCicUnifHint.empty_db;
         NRstatus.coerc_db = NCicCoercion.empty_db;
-        NRstatus.library_db = NCicLibrary.time0;
-        NRstatus.dump = fun x -> x;
+        NRstatus.library_db = NCicLibrary.time0 };
+       NRstatus.dump = []
       };
   }
 }