exception AlreadyDefined of UriManager.uri
-val merge_coercions: Cic.term -> Cic.term
+(* this is a pointer to the function which builds the inversion principle *)
+val build_inversion_principle: (UriManager.uri-> Cic.obj -> (UriManager.uri * Cic.obj) option) ref
(* adds an object to the library together with all auxiliary lemmas on it *)
(* (e.g. elimination principles, projections, etc.) *)
(* it returns the list of the uris of the auxiliary lemmas generated *)
-val add_obj: UriManager.uri -> Cic.obj -> basedir:string -> UriManager.uri list
+val add_obj:
+ RefinementTool.kit ->
+ UriManager.uri -> Cic.obj ->
+ UriManager.uri list
(* inverse of add_obj; *)
(* Warning: it does not remove the dependencies on the object and on its *)
(* is true are added to the library. *)
(* The list of added objects is returned. *)
val add_coercion:
- basedir:string -> add_composites:bool -> UriManager.uri ->
+ add_composites:bool ->
+ RefinementTool.kit -> UriManager.uri ->
UriManager.uri list
(* inverse of add_coercion, removes both the eventually created composite *)