+type coercion_decl =
+ UriManager.uri -> int (* arity *) ->
+ int (* saturations *) -> string (* baseuri *) ->
+ UriManager.uri list (* lemmas (new objs) *)
+
+(* the add_single_obj fun passed to the callback can raise AlreadyDefined *)
+val add_object_declaration_hook :
+ (add_obj:(UriManager.uri -> Cic.obj -> UriManager.uri list) ->
+ add_coercion:coercion_decl ->
+ UriManager.uri -> Cic.obj -> UriManager.uri list) -> unit
+