X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.mli;h=e6d7e46b30042778b6b3889970c56dac329741bd;hb=4f2e7eacea9e8b3089a575d7bf529fd5e70e8453;hp=d8a8b0574de506f222da61acfb073f9074723896;hpb=abd2098b6c4a40b36bb4b950c607eb4b4a7852bc;p=helm.git diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index d8a8b0574..e6d7e46b3 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -41,7 +41,7 @@ type coerc_carr = 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 @@ -60,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