X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FcicCoercion.ml;h=6f2443e98a45798f511279a0c5dd74e0a7e5bd07;hb=d7227b93729c13636d297b959b7d8c178dfe3aaf;hp=d7ad886b2c8fa33a07213faf7ea8b98bb9e974b4;hpb=9747f688a8624d819e07e7139df68a919f76b07d;p=helm.git diff --git a/components/library/cicCoercion.ml b/components/library/cicCoercion.ml index d7ad886b2..6f2443e98 100644 --- a/components/library/cicCoercion.ml +++ b/components/library/cicCoercion.ml @@ -302,7 +302,7 @@ let number_if_already_defined buri name l = (* given a new coercion uri from src to tgt returns * a list of (new coercion uri, coercion obj, universe graph) *) -let close_coercion_graph rt src tgt uri = +let close_coercion_graph rt src tgt uri baseuri = (* check if the coercion already exists *) let coercions = CoercDb.to_list () in let todo_list = get_closure_coercions src tgt uri coercions in @@ -334,9 +334,8 @@ let close_coercion_graph rt src tgt uri = let name_tgt = CoercDb.name_of_carr tgt in let by = List.map UriManager.name_of_uri l in let name = mangle name_tgt name_src by in - let buri = UriManager.buri_of_uri uri in let c_uri = - number_if_already_defined buri name + number_if_already_defined baseuri name (List.map (fun (_,_,u,_) -> u) acc) in let named_obj =