*)
let get_type msg st bo =
try
- let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.empty_ugraph in
+ let ty, _ = TC.type_of_aux' [] st.context (H.cic bo) Un.oblivion_ugraph in
ty
with e -> failwith (msg ^ ": " ^ Printexc.to_string e)
let get_ind_names uri tno =
try
- let ts = match E.get_obj Un.empty_ugraph uri with
+ let ts = match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (ts, _, _, _), _ -> ts
| _ -> assert false
in