X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_engine%2FgrafiteSync.ml;h=b6b9f7e5a27a8219091e9a1a361cf4a88f68b9f5;hb=f919cce8d299eab1dda92af4c5b53a8a7ac348af;hp=d318d11a73cb504b788dd98aa45cf18d66f635ba;hpb=5c1b44dfefa085fbb56e23047652d3650be9d855;p=helm.git

diff --git a/helm/software/components/grafite_engine/grafiteSync.ml b/helm/software/components/grafite_engine/grafiteSync.ml
index d318d11a7..b6b9f7e5a 100644
--- a/helm/software/components/grafite_engine/grafiteSync.ml
+++ b/helm/software/components/grafite_engine/grafiteSync.ml
@@ -58,9 +58,9 @@ let add_obj refinement_toolkit uri obj status =
  let lemmas = LibrarySync.add_obj refinement_toolkit uri obj in
  let add_to_universe (universe,status) uri =
    let term = CicUtil.term_of_uri uri in
-   let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.empty_ugraph in
+   let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
 (* prop filtering
-   let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.empty_ugraph in
+   let sort,_ = CicTypeChecker.type_of_aux' [] [] ty CicUniv.oblivion_ugraph in
    prerr_endline (CicPp.ppterm term);
    prerr_endline (CicPp.ppterm sort);
    let tkeys =