]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/cicCoercion.ml
- components: composed coercions mus be generated with current base uri
[helm.git] / components / library / cicCoercion.ml
index d7ad886b2c8fa33a07213faf7ea8b98bb9e974b4..6f2443e98a45798f511279a0c5dd74e0a7e5bd07 100644 (file)
@@ -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 =