From 476120b3d6bbe1372281fc5ad1c3a72a4954b546 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 2 Sep 2005 09:42:01 +0000 Subject: [PATCH] Missing initialization of the trusting function (for the kernel). --- helm/matita/matitacLib.ml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/helm/matita/matitacLib.ml b/helm/matita/matitacLib.ml index ebf1e455b..9165d5a8b 100644 --- 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 -- 2.39.2