X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.mli;h=3071aecc4eb724064849f21da4fc8bcc8314d099;hb=f93b83e4e8af580bc627ea0e8e601f0333c63df2;hp=e6d7e46b30042778b6b3889970c56dac329741bd;hpb=4f2e7eacea9e8b3089a575d7bf529fd5e70e8453;p=helm.git diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index e6d7e46b3..3071aecc4 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -48,16 +48,20 @@ 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 + +type coerc_db +val dump: unit -> coerc_db +val restore: coerc_db -> unit 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