val close_coercion_graph:
CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj)
- list
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri *
+ int (* saturations *) * Cic.obj * int (* arity *) * int (* cpos *)) list
exception UnableToCompose
val generate_composite:
- Cic.term -> Cic.term -> Cic.context ->
- Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) ->
+ Cic.term -> Cic.term (* t2 *) -> Cic.context ->
+ Cic.metasenv -> CicUniv.universe_graph ->
+ int -> int (* saturations of t1/t2 *) ->
Cic.term * Cic.metasenv * CicUniv.universe_graph