let f =
open_out
(Filename.dirname fname ^ "/" ^ mangled_baseuri ^ ".ml") in
- LibrarySync.set_object_declaration_hook
- (fun _ obj ->
+ LibrarySync.add_object_declaration_hook
+ (fun ~add_obj ~add_coercion _ obj ->
output_string f (CicExportation.ppobj baseuri obj);
- flush f);
+ flush f; []);
;;
let compile options fname =
;;
let build options fname =
+ let matita_debug = Helm_registry.get_bool "matita.debug" in
let compile opts fname =
try
GrafiteSync.push ();
GrafiteParser.pop ();
GrafiteSync.pop ();
false
- | exn ->
+ | exn when not matita_debug ->
HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
assert false
in