* http://cs.unibo.it/helm/.
*)
+
+ (** THIS MODULE SHOULD BE USED ONLY BY CoercGraph/CicCoercion/librarySync
+ *
+ * and may be merged with CicCoercion...
+ *
+ * **)
+
+
(** XXX WARNING: non-reentrant *)
type coerc_carr = Uri of UriManager.uri | Sort of Cic.sort | Term of Cic.term
exception EqCarrNotImplemented of string Lazy.t
val coerc_carr_of_term: Cic.term -> coerc_carr
val name_of_carr: coerc_carr -> string
-val use_coercions: bool ref (** initial status is true *)
-
val to_list:
unit ->
(coerc_carr * coerc_carr * UriManager.uri) list
val remove_coercion:
(coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
-val find_coercion:
+val find_coercion:
(coerc_carr * coerc_carr -> bool) -> UriManager.uri list
+val is_a_coercion: UriManager.uri -> bool
+val get_carr: UriManager.uri -> coerc_carr * coerc_carr
+
+val term_of_carr: coerc_carr -> Cic.term