many changes regarding coercions:

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

diff --git a/helm/software/matita/matitacLib.ml b/helm/software/matita/matitacLib.ml
index a9172cee5a563b43406d37873a7eea76a72ee354..ff9fb1d73629a468b1cde028505c56eb7385a6e3 100644 (file)
--- 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 =