X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcoercDb.mli;h=5f455c2af97dd6146bddeebd64c0f281ce0b6334;hb=6a25db65c9a787daf7344e3b166b2d798b1ff1a5;hp=92d4b7f2484e231e1547a62899fe094ece785c79;hpb=7f21c77a04c282e789dfbedf202fe90e15a7fde2;p=helm.git diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index 92d4b7f24..5f455c2af 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -36,6 +36,8 @@ 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 @@ -58,6 +60,8 @@ val find_coercion: (coerc_carr * coerc_carr -> bool) -> UriManager.uri 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