Bug: let-ins are always automatically folded!

[helm.git] / helm / software / matita / matitaInit.ml

diff --git a/helm/software/matita/matitaInit.ml b/helm/software/matita/matitaInit.ml
index 129f2dabdce3545fc5efe7b185fc801b3fc791c7..f75cbcf483472fd9d6d091315b108ec69f46bdbe 100644 (file)
--- 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 ()
+;;