X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;h=086932f6fab3ac8c5b4c5147561fc1374911abfc;hb=aa0d60227b785da3355b31519ba11cb4fbd2c925;hp=44f6681833c40408e75dc3ec61f6ba46db95be86;hpb=7b995596c8b11be95c430646227d01928cc71219;p=helm.git

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index 44f668183..086932f6f 100644
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -23,10 +23,12 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 open Printf
 
 type thingsToInitilaize = 
-  ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
+  ConfigurationFile | Db | Environment | Getter | Makelib | CmdLine
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -81,16 +83,6 @@ let initialize_makelib init_status =
   else
     init_status
 
-let initialize_notation init_status = 
-  wants [ConfigurationFile] init_status;
-  if not (already_configured [Notation] init_status) then
-    begin
-      CicNotation2.load_notation BuildTimeConf.core_notation_script;
-      Notation::init_status
-    end
-  else
-    init_status
-
 let initialize_environment init_status = 
   wants [ConfigurationFile] init_status;
   if not (already_configured [Getter;Environment] init_status) then
@@ -215,7 +207,7 @@ let initialize_all () =
   status := 
     List.fold_left (fun s f -> f s) !status
       [ parse_cmdline; load_configuration; initialize_makelib;
-        initialize_db; initialize_environment; initialize_notation ]
+        initialize_db; initialize_environment ]
 (*     initialize_notation 
       (initialize_environment 
         (initialize_db 
@@ -226,9 +218,6 @@ let initialize_all () =
 let load_configuration_file () =
   status := load_configuration !status
 
-let initialize_notation () =
-  status := initialize_notation (load_configuration !status)
-
 let parse_cmdline () =
   status := parse_cmdline !status