X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaInit.ml;h=f75cbcf483472fd9d6d091315b108ec69f46bdbe;hb=eff920e57112c3eaee889384d435602e41951a36;hp=129f2dabdce3545fc5efe7b185fc801b3fc791c7;hpb=662f191b09d1b9e3d13e4f9ee5c174c1ac08fadb;p=helm.git

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 129f2dabd..f75cbcf48 100644
--- a/helm/software/matita/matitaInit.ml
+++ b/helm/software/matita/matitaInit.ml
@@ -170,10 +170,6 @@ let extra_cmdline_specs = ref []
 let add_cmdline_spec l = extra_cmdline_specs := l @ !extra_cmdline_specs
 
 let parse_cmdline init_status =
-  let dump fname = 
-     let atexit = MatitacLib.dump fname in
-     at_exit atexit
-  in
   if not (already_configured [CmdLine] init_status) then begin
     wants [Registry] init_status;
     let includes = ref [] in
@@ -221,8 +217,6 @@ let parse_cmdline init_status =
               Helm_registry.set_bool "matita.system" true),
             ("Act on the system library instead of the user one"
              ^ "\n    WARNING: not for the casual user");
-        "-dump", Arg.String dump,
-          "<filename> Dump with expanded macros to <filename>";
         "-v", 
           Arg.Unit (fun () -> Helm_registry.set_bool "matita.verbose" true), 
           "Verbose mode";
@@ -235,7 +229,7 @@ let parse_cmdline init_status =
               ("Do not catch top-level exception "
               ^ "(useful for backtrace inspection)");
 	    "-onepass",
-	    Arg.Unit (fun () -> GrafiteDisambiguator.only_one_pass := true),
+	    Arg.Unit (fun () -> MultiPassDisambiguator.only_one_pass := true),
 	    "Enable only one disambiguation pass";    
           ]
         else []
@@ -286,4 +280,8 @@ let initialize_environment () =
   status := initialize_environment !status
 
 let _ =
-  Inversion_principle.init ()
+  CicFix.init ();
+  Inversion_principle.init ();
+  CicRecord.init ();
+  CicElim.init ()
+;;