* http://cs.unibo.it/helm/.
*)
+type coercion_search_result =
+ | SomeCoercion of Cic.term
+ | NoCoercion
+ | NotMetaClosed
+ | NotHandled of string Lazy.t
+
val look_for_coercion :
- UriManager.uri -> UriManager.uri -> Cic.term option
+ Cic.term -> Cic.term -> coercion_search_result
+(* also adds them to the Db *)
val close_coercion_graph:
- UriManager.uri -> UriManager.uri -> UriManager.uri ->
+ CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
(UriManager.uri * Cic.obj * CicUniv.universe_graph) list
-val get_coercions_list:
- unit -> (UriManager.uri * UriManager.uri * UriManager.uri) list
-