X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FcicCoercion.ml;h=b45599ceb5efd3ca6893365a78c107bf4a25223f;hb=d35aca0e979a9c7edbc60c44040360d52be8ca82;hp=42a19bcf92fcea3cbcab72129101c62ea0a87b27;hpb=e53dfd3fa17a77ab1fdd249ed2e5b6d0f9d94d88;p=helm.git diff --git a/helm/software/components/library/cicCoercion.ml b/helm/software/components/library/cicCoercion.ml index 42a19bcf9..b45599ceb 100644 --- a/helm/software/components/library/cicCoercion.ml +++ b/helm/software/components/library/cicCoercion.ml @@ -26,14 +26,15 @@ (* $Id$ *) let close_coercion_graph_ref = ref - (fun _ _ _ _ -> [] : - CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> + (fun _ _ _ _ _ -> [] : + CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int -> string (* baseuri *) -> - (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * Cic.obj) list) + (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * + int * int) list) ;; let set_close_coercion_graph f = close_coercion_graph_ref := f;; -let close_coercion_graph c1 c2 u s = - !close_coercion_graph_ref c1 c2 u s +let close_coercion_graph c1 c2 u sat s = + !close_coercion_graph_ref c1 c2 u sat s ;;