X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Flibrary%2FlibrarySync.ml;h=a09baafe1a99fe8e3fdc1aeed08451bbc706dd9d;hb=cbf47ddef11207628a9838973a192566e1e60ba7;hp=9ce5801fdb12cdc9a98246f30b3fe6ba76d8434f;hpb=5cb95a2e44f979183a8c3e39baa3b4e7cfaf8182;p=helm.git

diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml
index 9ce5801fd..a09baafe1 100644
--- a/components/library/librarySync.ml
+++ b/components/library/librarySync.ml
@@ -84,7 +84,7 @@ let save_object_to_disk uri obj ugraph univlist =
   (univgraphuri,xmlunivgraphpath) ::
     (* now the optional body, both write and register *)
     (match bodyxml,bodyuri with
-       None,None -> []
+       None,_ -> []
      | Some bodyxml,Some bodyuri->
          ensure_path_exists xmlbodypath;
          Xml.pp ~gzip:true bodyxml (Some xmlbodypath);
@@ -227,29 +227,41 @@ let add_coercion ~add_composites refinement_toolkit uri =
   List.iter 
     (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
       new_coercions;
-  CoercDb.add_coercion (src_carr, tgt_carr, uri);
-  (* add the composites obj and they eventual lemmas *)
-  let lemmas = 
-    if add_composites then
-      List.fold_left
-        (fun acc (_,_,uri,obj) -> 
-          add_single_obj uri obj refinement_toolkit;
-          uri::acc) 
-        composite_uris new_coercions
-    else
+  if 
+    List.exists 
+      (fun (s,t,_) -> CoercDb.eq_carr s src_carr && CoercDb.eq_carr t tgt_carr)
+      (CoercDb.to_list ())
+  then
+    begin
+      assert (new_coercions = []);
       []
-  in
-  (* store that composite_uris are related to uri. the first component is the
-   * stuff in the DB while the second is stuff for remove_obj *)
-  (* 
-     prerr_endline ("adding: " ^ 
-       string_of_bool add_composites ^ UriManager.string_of_uri uri);
-     List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
-      composite_uris; 
-  *)
-  UriManager.UriHashtbl.add coercion_hashtbl uri 
-    (composite_uris,if add_composites then composite_uris else []);
-  lemmas
+    end
+  else
+    begin
+      CoercDb.add_coercion (src_carr, tgt_carr, uri);
+      (* add the composites obj and they eventual lemmas *)
+      let lemmas = 
+        if add_composites then
+          List.fold_left
+            (fun acc (_,_,uri,obj) -> 
+              add_single_obj uri obj refinement_toolkit;
+              uri::acc) 
+            composite_uris new_coercions
+        else
+          []
+      in
+      (* store that composite_uris are related to uri. the first component is
+       * the stuff in the DB while the second is stuff for remove_obj *)
+      (* 
+         prerr_endline ("adding: " ^ 
+           string_of_bool add_composites ^ UriManager.string_of_uri uri);
+         List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
+          composite_uris; 
+      *)
+      UriManager.UriHashtbl.add coercion_hashtbl uri 
+        (composite_uris,if add_composites then composite_uris else []);
+      lemmas
+    end
 
 let remove_coercion uri =
   try