X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=a0a0f324efe7352ee2496ccca2d1f30f0321f1aa;hb=a631b7a0a43b178eb7f68efb4345302441067dcd;hp=da2d69ec11352c6571b29673ae55391e37a2c743;hpb=7f492f1ed0024596094fc6585c604fd814ea8b60;p=helm.git

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index da2d69ec1..a0a0f324e 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -325,10 +325,18 @@ and
                  CicPp.ppterm (Cic.Sort s1) ^ " <> " ^ 
                  CicPp.ppterm (Cic.Sort s2)); false)
              | _ -> 
+                let ty', _ = 
+                  CicTypeChecker.type_of_aux' [] [] (CicUtil.term_of_uri u) 
+                  CicUniv.oblivion_ugraph
+                in
+                if CicUtil.alpha_equivalence ty ty' then
                 (HLog.warn 
                 ("Skipping coercion " ^ UriManager.name_of_uri uri ^ " since "^
                  "it is a duplicate of " ^ UriManager.string_of_uri u);
-                true))
+                true)
+                else false
+                
+                )
          ul)
       (CoercDb.to_list ())
   in