* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
+
+ (** 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
+exception EqCarrOnNonMetaClosed
+val eq_carr: coerc_carr -> coerc_carr -> bool
+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:
+val to_list:
unit ->
- (UriManager.uri * UriManager.uri * UriManager.uri) list
+ (coerc_carr * coerc_carr * UriManager.uri) list
val add_coercion:
- UriManager.uri * UriManager.uri * UriManager.uri -> unit
+ coerc_carr * coerc_carr * UriManager.uri -> unit
val remove_coercion:
- (UriManager.uri * UriManager.uri * UriManager.uri -> bool) -> unit
+ (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
val find_coercion:
- (UriManager.uri * UriManager.uri -> bool) -> UriManager.uri list
+ (coerc_carr * coerc_carr -> bool) -> UriManager.uri list