Missing initialization of the trusting function (for the kernel).

diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml
index ebf1e455bff5d62f4cd9d28f0e0be43441811603..9165d5a8b7e6ec659a142993cc678ab8d8a2376a 100644 (file)
--- a/helm/matita/matitacLib.ml
+++ b/helm/matita/matitacLib.ml
@@ -134,8 +134,12 @@ let rec interactive_loop () =
 
 let go () =
   Helm_registry.load_from BuildTimeConf.matita_conf;
+  CicNotation.load_notation BuildTimeConf.core_notation_script;
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
+  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));
   Sys.catch_break true;
   interactive_loop ()
@@ -153,6 +157,9 @@ let main ~mode =
   Http_getter.init ();
   MetadataTypes.ownerize_tables (Helm_registry.get "matita.owner");
   MatitaDb.create_owner_environment ();
+  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));
   Sys.catch_break true;
   let origcb = MatitaLog.get_log_callback () in