X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=4dc20f77fa968ed961361a7449c69646d06b8037;hb=4216d3e6b09d1be8784ee9394f6c7f5aed4300a7;hp=a3429840b7b2e169c835c753529de9e4cabed0e3;hpb=4f9820060bce92cfdb862b3c699e96c20c64a051;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index a3429840b..4dc20f77f 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -173,8 +173,8 @@ let remove_single_obj uri =
    (fun uri -> 
      ignore (LibraryDb.remove_uri uri);
      (*CoercGraph.remove_coercion uri;*)
-     CicEnvironment.remove_obj uri
-   ) uris_to_remove
+   ) uris_to_remove ;
+  CicEnvironment.remove_obj uri
 
 (*** GENERATION OF AUXILIARY LEMMAS ***)
 
@@ -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;