X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=2dcd6a8b9c8b4c4aae69a4ccadd4cf81c8529b75;hb=15469f16ff6f86c6cc0107070775b6c03c0ec478;hp=9ce5801fdb12cdc9a98246f30b3fe6ba76d8434f;hpb=ee3f8d6fa92b051394a2ff7c71c03ac33a05182b;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 9ce5801fd..2dcd6a8b9 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -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