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 =