milestone in basic_2, λδ-2A reconstructed

[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 da2d69ec11352c6571b29673ae55391e37a2c743..185ae53158f7cff7061382b12fbbc7f89f2974aa 100644 (file)
--- 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