X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.mli;h=d8e432e75b9035888478ed3d1277dbe730344dcc;hb=95bd260f9bcfd158941fa018fceabc917a77ac96;hp=61e2b2515ae9ba36837b142427cfd508b12014a5;hpb=2aad3e4b468d3e4199712437e7ef82afbbc9553d;p=helm.git

diff --git a/helm/software/components/library/librarySync.mli b/helm/software/components/library/librarySync.mli
index 61e2b2515..d8e432e75 100644
--- a/helm/software/components/library/librarySync.mli
+++ b/helm/software/components/library/librarySync.mli
@@ -25,6 +25,8 @@
 
 exception AlreadyDefined of UriManager.uri
 
+val set_object_declaration_hook : (UriManager.uri -> Cic.obj -> unit) -> unit
+
 (* this is a pointer to the function which builds the inversion principle *)
 val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) list) ref
 
@@ -47,8 +49,9 @@ val remove_obj: UriManager.uri -> unit
 (* The list of added objects is returned.                                *)
 val add_coercion: 
   add_composites:bool -> 
-  RefinementTool.kit -> UriManager.uri -> 
-    UriManager.uri list
+  RefinementTool.kit -> UriManager.uri -> int (* arity *) ->
+   int (* saturations *) -> string (* baseuri *) ->
+    (UriManager.uri * int * int) list (* URI, arity, saturations *)
 
 (* inverse of add_coercion, removes both the eventually created composite   *)
 (* coercions and the information that [uri] and the composites are coercion *)