X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.mli;h=d8a8b0574de506f222da61acfb073f9074723896;hb=9897efac755aac85095075b7e0a967fe340092c1;hp=1f5df89334352f3a299d5ee83ec8f044005c68a3;hpb=9393a9f9370014c904244358abe4ec6e11a9d158;p=helm.git diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index 1f5df8933..d8a8b0574 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -36,16 +36,19 @@ type coerc_carr = | 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 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 + (coerc_carr * coerc_carr * UriManager.uri list) list val add_coercion: coerc_carr * coerc_carr * UriManager.uri -> unit