X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaInit.ml;fp=helm%2Fmatita%2FmatitaInit.ml;h=9ea9e07d2670d89729b3b9fe5eafbbc9487a928f;hb=6fa89cef6aa8fc1774db065a9fcfc47867579054;hp=e69c22cf87a7897f36c1c071df9c6e4c221a37d0;hpb=aaf75c2cff13515b049a15cc8a96734e8967ae9b;p=helm.git

diff --git a/helm/matita/matitaInit.ml b/helm/matita/matitaInit.ml
index e69c22cf8..9ea9e07d2 100644
--- a/helm/matita/matitaInit.ml
+++ b/helm/matita/matitaInit.ml
@@ -26,8 +26,7 @@
 open Printf
 
 type thingsToInitilaize = 
-  ConfigurationFile | Db | Environment | Getter | Notation | 
-  Paramodulation | Makelib | CmdLine
+  ConfigurationFile | Db | Environment | Getter | Notation | Makelib | CmdLine
   
 exception FailedToInitialize of thingsToInitilaize
 
@@ -61,16 +60,6 @@ let initialize_db init_status =
   else
     init_status
 
-let initialize_paramodulation init_status = 
-  wants [] init_status;
-  if not (already_configured [Paramodulation] init_status) then
-    begin
-      Paramodulation.Saturation.init ();
-      Paramodulation::init_status
-    end
-  else
-    init_status
-
 let initialize_makelib init_status = 
   wants [ConfigurationFile] init_status;
   if not (already_configured [Makelib] init_status) then
@@ -207,13 +196,15 @@ let die_usage () =
 
 let initialize_all () =
   status := 
-    initialize_notation 
+    List.fold_left (fun s f -> f s) !status
+      [ parse_cmdline; load_configuration; initialize_makelib;
+        initialize_db; initialize_environment; initialize_notation ]
+(*     initialize_notation 
       (initialize_environment 
         (initialize_db 
-          (initialize_paramodulation 
-            (initialize_makelib
-              (load_configuration
-                (parse_cmdline !status))))))
+          (initialize_makelib
+            (load_configuration
+              (parse_cmdline !status))))) *)
 
 let load_configuration_file () =
   status := load_configuration !status