let fst3 (x, _, _) = x
let refine c t =
- try let t, _, _, _ = Rf.type_of_aux' [] c t Un.empty_ugraph in t
+ try let t, _, _, _ = Rf.type_of_aux' [] c t Un.oblivion_ugraph in t
with e ->
Printf.eprintf "REFINE EROR: %s\n" (Printexc.to_string e);
Printf.eprintf "Ref: context: %s\n" (Pp.ppcontext c);
raise e
let get_type c t =
- try let ty, _ = TC.type_of_aux' [] c t Un.empty_ugraph in ty
+ try let ty, _ = TC.type_of_aux' [] c t Un.oblivion_ugraph in ty
with e ->
Printf.eprintf "TC: context: %s\n" (Pp.ppcontext c);
Printf.eprintf "TC: term : %s\n" (Pp.ppterm t);
let is_atomic t = not (is_not_atomic t)
let get_ind_type uri tyno =
- match E.get_obj Un.empty_ugraph uri with
+ match E.get_obj Un.oblivion_ugraph uri with
| C.InductiveDefinition (tys, _, lpsno, _), _ -> lpsno, List.nth tys tyno
| _ -> assert false