X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitacLib.ml;h=ff9fb1d73629a468b1cde028505c56eb7385a6e3;hb=798c509fb17048996eb30fb991cc2da21d07dfcb;hp=f248545fba8c6d5caae409eb43fee604273185b2;hpb=7a3c40d0d56ba3c20126f1d2c9f651adc95eaef7;p=helm.git

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index f248545fb..ff9fb1d73 100644
--- a/helm/software/matita/matitacLib.ml
+++ b/helm/software/matita/matitacLib.ml
@@ -180,10 +180,10 @@ let activate_extraction baseuri fname =
   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 =
@@ -382,6 +382,7 @@ module F =
     ;;
 
     let build options fname =
+      let matita_debug = Helm_registry.get_bool "matita.debug" in
       let compile opts fname =
         try
           GrafiteSync.push ();
@@ -395,7 +396,7 @@ module F =
             GrafiteParser.pop ();
             GrafiteSync.pop ();
             false
-        | exn ->
+        | exn when not matita_debug ->
             HLog.error ("Unexpected " ^ snd(MatitaExcPp.to_string exn));
             assert false
       in