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
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";
("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 []
status := initialize_environment !status
let _ =
- Inversion_principle.init ()
+ CicFix.init ();
+ Inversion_principle.init ();
+ CicRecord.init ();
+ CicElim.init ()
+;;