call Unshare.fresh_types

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 203f78869b33aac4e75c65bb8355e9d9ea485c5d..8a0c2bcc4406f8832a2fbe0e6fac5300ee4232ba 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -128,7 +128,8 @@ let save_object_to_disk uri obj ugraph univlist =
 
 let typecheck_obj =
  let profiler = HExtlib.profile "add_obj.typecheck_obj" in
-  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri)
+  (Unshare.fresh_types obj)
 
 let index_obj =
  let profiler = HExtlib.profile "add_obj.index_obj" in