X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=638c0ce64a81d037749048c9a698362bde6b0916;hb=b44a732a930584aa08f4a78371dd9ac5b405f31e;hp=fe1c961fb3c8dd7791250ee97e783b56fa30584f;hpb=936f80cf031a7b034dd70fef49abb90e69f2e680;p=helm.git

diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml
index fe1c961fb..638c0ce64 100644
--- a/components/library/cicCoercion.ml
+++ b/components/library/cicCoercion.ml
@@ -27,14 +27,13 @@
 
 let close_coercion_graph_ref = ref
  (fun _ _ _ _ _ -> [] : 
-   RefinementTool.kit -> 
-   CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri ->
+   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) list)
 ;;
 
 let set_close_coercion_graph f = close_coercion_graph_ref := f;;
 
-let close_coercion_graph r c1 c2 u s = 
-  !close_coercion_graph_ref r c1 c2 u s
+let close_coercion_graph c1 c2 u sat s = 
+  !close_coercion_graph_ref c1 c2 u sat s
 ;;