X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Flibrary%2FlibrarySync.ml;h=185ae53158f7cff7061382b12fbbc7f89f2974aa;hb=0c302a9fda708e5019e48d14c5419a8a65190745;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..185ae5315 100644
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -325,12 +325,20 @@ 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 ())
+      (CoercDb.to_list (CoercDb.dump ()))
   in
   let cpos = no_args - arity - saturations - 1 in 
   if not add_composites then