From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 11 Apr 2008 15:15:46 +0000 (+0000)
Subject: call Unshare.fresh_types
X-Git-Tag: make_still_working~5353
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=481ad7e9dbc461e8f1b4a71aa85fa83500173329;p=helm.git

call Unshare.fresh_types
---

diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml
index 203f78869..8a0c2bcc4 100644
--- 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