more composites to make all happy!

[helm.git] / helm / software / components / library / librarySync.ml

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 13596c84e27e696b91168d8c2086da8cdeeea0fd..e6871b60ee8254d02d68229a61de1d71a11f3b97 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -331,7 +331,12 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
            CoercDb.eq_carr t tgt_carr &&
            if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
            CicUniv.oblivion_ugraph)
-           then true else
+           then 
+             (HLog.warn 
+               ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since " ^
+               "it is a duplicate of " ^ UriManager.string_of_uri u);
+             true) 
+           else
             (HLog.warn
               ("Coercions " ^ 
                 UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri