oblivion ugraph everywhere outside the kernel

[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 203f78869b33aac4e75c65bb8355e9d9ea485c5d..fd89f77c8f7e89744e7a745bd8ff16f5df094b79 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
@@ -228,7 +229,7 @@ let generate_elimination_principles uri refinement_toolkit =
        List.iter remove_single_obj !uris;
        raise exn 
   in
-  let (obj, univ) = (CicEnvironment.get_obj CicUniv.empty_ugraph uri) in
+  let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
     match obj with
       | Cic.InductiveDefinition (indTypes, _, _, _) ->
          let counter = ref 0 in
@@ -272,7 +273,7 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations
 =
   let coer_ty,_ =
     let coer = CicUtil.term_of_uri uri in
-    CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_ugraph 
+    CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph 
   in
   (* we have to get the source and the tgt type uri
    * in Coq syntax we have already their names, but
@@ -419,8 +420,8 @@ let generate_projections refinement_toolkit uri fields =
     (fun (uri, name, bo) (_name, coercion, arity) ->
       let saturations = 0 in
       try
-       let ty, ugraph =
-         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
+       let ty, _ =
+         CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
        let attrs = [`Class `Projection; `Generated] in
        let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
         add_single_obj uri obj refinement_toolkit;