| Uri of UriManager.uri (* const, mutind, mutconstr *)
| Sort of Cic.sort (* Prop, Set, Type *)
| Term of Cic.term (* nothing supported *)
+ | Fun of int
+;;
exception EqCarrNotImplemented of string Lazy.t
exception EqCarrOnNonMetaClosed
-val eq_carr: coerc_carr -> coerc_carr -> bool
+val eq_carr: ?exact:bool -> coerc_carr -> coerc_carr -> bool
val coerc_carr_of_term: Cic.term -> coerc_carr
val name_of_carr: coerc_carr -> string
+val uri_of_carr: coerc_carr -> UriManager.uri option
val to_list:
unit ->
- (coerc_carr * coerc_carr * UriManager.uri list) list
+ (coerc_carr * coerc_carr * (UriManager.uri * int) list) list
val add_coercion:
- coerc_carr * coerc_carr * UriManager.uri -> unit
+ coerc_carr * coerc_carr * UriManager.uri * int -> unit
val remove_coercion:
- (coerc_carr * coerc_carr * UriManager.uri -> bool) -> unit
+ (coerc_carr * coerc_carr * UriManager.uri * int -> bool) -> unit
val find_coercion:
- (coerc_carr * coerc_carr -> bool) -> UriManager.uri list
+ (coerc_carr * coerc_carr -> bool) -> (UriManager.uri * int) list
val is_a_coercion: UriManager.uri -> bool
+val is_a_coercion': Cic.term -> bool
+val is_a_coercion_to_funclass: Cic.term -> int option
val get_carr: UriManager.uri -> coerc_carr * coerc_carr
val term_of_carr: coerc_carr -> Cic.term