MatitaInit.initialize_all ();
(* must be called after init since args are set by cmdline parsing *)
let fname = fname () in
+ if false then
+ let basename = Filename.chop_extension fname in
+ let f = open_out (basename ^ ".ml") in
+ LibrarySync.set_object_declaration_hook
+ (fun _ obj ->
+ output_string f (CicExportation.ppobj (Filename.basename basename) obj);
+ flush f);
let system_mode = Helm_registry.get_bool "matita.system" in
let bench_mode = Helm_registry.get_bool "matita.bench" in
if bench_mode then
LibraryMisc.lexicon_file_of_baseuri
~must_exist:false ~baseuri ~writable:true
in
- GrafiteMarshal.save_moo moo_fname moo_content_rev;
- LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+(* FG: we do not generate .moo when dumping .mma files *)
+ if Helm_registry.get_bool "matita.moo" then begin
+ GrafiteMarshal.save_moo moo_fname moo_content_rev;
+ LexiconMarshal.save_lexicon lexicon_fname lexicon_content_rev;
+ end;
HLog.message
(sprintf "execution of %s completed in %s." fname (hou^min^sec));
pp_times fname bench_mode true big_bang;