]> matita.cs.unibo.it Git - helm.git/blobdiff - components/library/librarySync.ml
- components: composed coercions mus be generated with current base uri
[helm.git] / components / library / librarySync.ml
index 5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf..4dc20f77fa968ed961361a7449c69646d06b8037 100644 (file)
@@ -211,7 +211,7 @@ let remove_all_coercions () =
   UriManager.UriHashtbl.clear coercion_hashtbl;
   CoercDb.remove_coercion (fun (_,_,u1) -> true)
 
-let add_coercion ~add_composites refinement_toolkit uri arity =
+let add_coercion ~add_composites refinement_toolkit uri arity baseuri =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
     CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
@@ -270,6 +270,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity =
   else
     let new_coercions = 
       CicCoercion.close_coercion_graph refinement_toolkit src_carr tgt_carr uri 
+       baseuri
     in
     let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
     if already_in then
@@ -359,6 +360,7 @@ let generate_projections refinement_toolkit uri fields =
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
               let x = 
                 add_coercion ~add_composites:true refinement_toolkit uri arity
+                (UriManager.buri_of_uri uri)
               in
 (*prerr_endline ("are: ");
   List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;