exception AlreadyDefined of UriManager.uri
-val merge_coercions: Cic.term -> Cic.term
-
(* 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 -> basedir:string ->
+ 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 ->
+ basedir:string -> add_composites:bool ->
+ RefinementTool.kit -> UriManager.uri ->
UriManager.uri list
(* inverse of add_coercion, removes both the eventually created composite *)