(* it returns the list of the uris of the auxiliary lemmas generated *)
val add_obj:
RefinementTool.kit ->
- UriManager.uri -> Cic.obj -> basedir:string ->
+ UriManager.uri -> Cic.obj ->
UriManager.uri list
(* inverse of add_obj; *)
(* is true are added to the library. *)
(* The list of added objects is returned. *)
val add_coercion:
- basedir:string -> add_composites:bool ->
+ add_composites:bool ->
RefinementTool.kit -> UriManager.uri ->
UriManager.uri list