X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=4e64e6badc369c21d92e83d96c9719a4d72f1caa;hb=686ad41d7c9431094c12dae0fa6b84a898c38e84;hp=a3429840b7b2e169c835c753529de9e4cabed0e3;hpb=4b98f68b964c9f87868c445e794bc745a99d5b17;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index a3429840b..4e64e6bad 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/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
@@ -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
@@ -292,9 +293,10 @@ let add_coercion ~add_composites refinement_toolkit uri arity =
         let lemmas = 
           if add_composites then
             List.fold_left
-              (fun acc (_,_,uri,obj) -> 
+              (fun acc (_,tgt,uri,obj) -> 
                 add_single_obj uri obj refinement_toolkit;
-                uri::acc) 
+                let arity = match tgt with CoercDb.Fun n -> n | _ -> 0 in
+                 (uri,arity)::acc) 
               [] new_coercions
           else
             []
@@ -357,14 +359,19 @@ let generate_projections refinement_toolkit uri fields =
          if coercion then
             begin
 (*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
+              (*CSC: I think there is a bug here. The composite coercions
+                are not remembered in the .moo file. Thus they are re-generated
+                every time. Right? *)
               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;
   prerr_endline "---";
 *)
-              x
+              (*CSC: I throw the arity away. See comment above *)
+              List.map fst x
             end
           else  
             []