From 481ad7e9dbc461e8f1b4a71aa85fa83500173329 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 11 Apr 2008 15:15:46 +0000 Subject: [PATCH] call Unshare.fresh_types --- helm/software/components/library/librarySync.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- 2.39.2