X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcoercDb.mli;h=59c07f447acd3796130a16b2fc238b2e52969407;hb=0c302a9fda708e5019e48d14c5419a8a65190745;hp=83e61dbfba2f708097e12e7b04dcef6e6ffda710;hpb=84e6cbe962c9a534be48542c098d7bb0d90be9a1;p=helm.git diff --git a/helm/software/components/library/coercDb.mli b/helm/software/components/library/coercDb.mli index 83e61dbfb..59c07f447 100644 --- a/helm/software/components/library/coercDb.mli +++ b/helm/software/components/library/coercDb.mli @@ -37,15 +37,15 @@ val string_of_carr: coerc_carr -> string (* takes a term in whnf ~delta:false and a desired ariety *) val coerc_carr_of_term: Cic.term -> int -> coerc_carr -val to_list: - unit -> - (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list - type coerc_db val empty_coerc_db : coerc_db val dump: unit -> coerc_db val restore: coerc_db -> unit +val to_list: + coerc_db -> + (coerc_carr * coerc_carr * (UriManager.uri * int * int) list) list + (* src carr, tgt carr, uri, saturations, coerced position * invariant: * if the constant pointed by uri has n argments