Big commit to let Ferruccio try the merge_coercion patch.

[helm.git] / helm / matita / matitacLib.ml

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index 355ceed6044385e3e325ca9f73008b11ac26f37d..1f9dad80f7dbcf1815dbdf7123c6a7032a7e5945 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -123,7 +123,7 @@ let go () =
   CicEnvironment.set_trust (* environment trust *)
     (let trust = Helm_registry.get_bool "matita.environment_trust" in
      fun _ -> trust);
-  status := Some (ref (Lazy.force MatitaEngine.initial_status));
+  status := Some (ref (MatitaSync.init ()));
   Sys.catch_break true;
   interactive_loop ()
 
@@ -131,7 +131,7 @@ let main ~mode =
   MatitaInit.initialize_all ();
   (* must be called after init since args are set by cmdline parsing *)
   let fname = fname () in
-  status := Some (ref (Lazy.force MatitaEngine.initial_status));
+  status := Some (ref (MatitaSync.init ()));
   Sys.catch_break true;
   let origcb = HLog.get_log_callback () in
   let newcb tag s =