val look_for_coercion :
Cic.term -> Cic.term -> coercion_search_result
-(* also adds them to the Db *)
-val close_coercion_graph:
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
- (UriManager.uri * Cic.obj * CicUniv.universe_graph) list
+(* it returns the list of composite coercions and their auxiliary lemmas *)
+(* composite coercions are always declared as such; they are added to the *)
+(* library only on demand (i.e. not when processing a .moo) *)
+val add_coercion:
+ basedir:string -> add_composites:bool -> UriManager.uri -> UriManager.uri list
+val remove_coercion: UriManager.uri -> unit