]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/library/cicCoercion.ml
Fixed (yet another) nasty bug, in deep_eq this time
[helm.git] / helm / software / components / library / cicCoercion.ml
index 638c0ce64a81d037749048c9a698362bde6b0916..b45599ceb5efd3ca6893365a78c107bf4a25223f 100644 (file)
@@ -29,7 +29,8 @@ let close_coercion_graph_ref = ref
  (fun _ _ _ _ _ -> [] : 
    CoercDb.coerc_carr -> CoercDb.coerc_carr -> UriManager.uri -> int ->
    string (* baseuri *) ->
-     (CoercDb.coerc_carr * CoercDb.coerc_carr * UriManager.uri * int * Cic.obj * int) 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;;