X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=d5eca252afe3f935ef740e1f0e2a76df02c9d1c1;hb=6a25db65c9a787daf7344e3b166b2d798b1ff1a5;hp=5e8ddaf6d5db898229d0cd7aec7b1eb72bda2bcf;hpb=04e808fe2e4a18c868af334ad4a2c95b0040e58d;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 5e8ddaf6d..d5eca252a 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -111,7 +111,7 @@ let add_single_obj uri obj refinement_toolkit =
   let module RT = RefinementTool in
   let obj = 
     if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
-       not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
+       not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
     then
       refinement_toolkit.RT.pack_coercion_obj obj
     else
@@ -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;