(* This module implements the Coercions transitive closure *)
val close_coercion_graph:
- RefinementTool.kit ->
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
string (* baseuri *) ->
- (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list
+ (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj)
+ list
exception UnableToCompose
val generate_composite:
Cic.term -> Cic.term -> Cic.context ->
Cic.metasenv -> CicUniv.universe_graph -> int (* arity *) ->
- bool (* last lambda goes with innermost arg *) ->
Cic.term * Cic.metasenv * CicUniv.universe_graph