notation factored, coercion commant taking terms and not only URI

[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 fd89f77c8f7e89744e7a745bd8ff16f5df094b79..d70bd15453cea4b9562d7abf94db97d21eaf94ef 100644 (file)
--- a/helm/software/components/library/librarySync.ml
+++ b/helm/software/components/library/librarySync.ml
@@ -128,8 +128,7 @@ 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)
-  (Unshare.fresh_types obj)
+  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj
 
 let index_obj =
  let profiler = HExtlib.profile "add_obj.index_obj" in
@@ -160,8 +159,10 @@ let add_single_obj uri obj refinement_toolkit =
       (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
       (univ_time *. 100. /. total_time) (total_time) (univ_time)
       (UriManager.name_of_uri uri));*)
-    let _, ugraph, univlist = 
-      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
+    let obj, ugraph, univlist = 
+      try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
+      with CicEnvironment.Object_not_found _ -> assert false
+    in
     try 
       index_obj ~dbd ~uri; (* 2 must be in the env *)
       try