(* This module implements the Coercions transitive closure *)
val set_close_coercion_graph :
- (RefinementTool.kit ->
- CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+ (CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
string (* baseuri *) ->
(CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list)
-> unit
val close_coercion_graph:
- RefinementTool.kit ->
CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
string (* baseuri *) ->
(CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list